Stream: Isabelle/ML

Topic: Markup for arguments to custom commands

Hanno Becker (Oct 04 2023 at 08:22):

Hi! I'm trying to understand when/how clickable references to formal entities are created. Here's a minimal example:

theory Scratch
  imports Main
  keywords "dummy0" "dummy1" :: thy_goal
begin
ML‹
  fun do_something tyname ctxt =
    let val _ = Proof_Context.read_type_name {proper = true, strict = false} ctxt tyname in
       ctxt
    end
  fun do_nothing _ ctxt = ctxt
  val _ = Outer_Syntax.local_theory @{command_keyword "dummy0"} "" (Parse.const >> do_something)
  val _ = Outer_Syntax.local_theory @{command_keyword "dummy1"} "" (Parse.const >> do_nothing)
›
dummy0 nat ―‹Clickable reference›
dummy1 nat ―‹No reference›
end

How does Isabelle achieve the clickable reference to nat in case of dummy0 nat? Parse.const is a mere string parser, so where and how is the information about the position of the string retained that would later allow read_type_name to add markup?

Fabian Huch (Oct 04 2023 at 08:39):

A pide report is generated (see context_position.ML) and sent to Isabelle/Scala. Parse.const will not do that but Proof_Context.read_type_name will.

Hanno Becker (Oct 04 2023 at 08:41):

Thanks Fabian! But read_type_name takes a mere string as an argument, without positioning information? How/where is the position information about the original argument retained after Parse.term?

Fabian Huch (Oct 04 2023 at 08:50):

I assume that is stored in the context.

Hanno Becker (Oct 04 2023 at 08:50):

I'm sorry, I don't follow yet -- can you elaborate?

Fabian Huch (Oct 04 2023 at 08:57):

There is the ctxt argument in your do_* function -- this is a context where such arbitrary contextual information can be stored, and judging from the signatures, this is where the position comes from.

Fabian Huch (Oct 04 2023 at 08:57):

If you take a look at the definitions you should be able to follow how exactly.

Hanno Becker (Oct 04 2023 at 09:01):

Yes I saw that Parse.typ stores some information about the input being parsed 'as a type' somewhere. But even so, it only returns a plain string, so even with the context being passed around, I don't understand how read_type_name could know which source code position its input is coming from.

Fabian Huch (Oct 04 2023 at 09:10):

I'm not sure what you mean with 'only returns a plain string' - No method involved here does that ;)

Fabian Huch (Oct 04 2023 at 09:10):

There is read_type_name which takes a context

Fabian Huch (Oct 04 2023 at 09:11):

and Parse.const which is of type string parser.

Hanno Becker (Oct 04 2023 at 09:12):

Yes. Parse.const is a string parser, so the parser's output is a string -- ISTM that unless position information is somehow hidden in the string, read_type_name would not be able to add markup for it in the original source.

Hanno Becker (Oct 04 2023 at 09:17):

Ok... that does indeed seem to be the case. String.explode shows various positioning information in the string that are not displayed when printing it e.g. via tracing

Hanno Becker (Oct 04 2023 at 09:19):

ML‹
  fun do_something tyname ctxt =
    let
       val _ = tyname |> String.explode |> List.map Char.toString |> String.concatWith "" |> tracing
       val _ = Proof_Context.read_type_name {proper = true, strict = false} ctxt tyname in
       ctxt
    end
  val _ = Outer_Syntax.local_theory @{command_keyword "dummy0"} "" (Parse.typ >> do_something)
›

dummy0 nat ―‹Clickable reference›
―‹\^E\^Finput\^Fdelimited=false\^Foffset=8\^Fend_offset=11\^Fid=-15172\^Enat\^E\^F\^E›

Fabian Huch (Oct 04 2023 at 09:20):

Also the string parser is not a function to string - it is T list -> 'a * T list, and the whole parser for the command is of type (local_theory -> local_theory) parser.

Hanno Becker (Oct 04 2023 at 09:20):

Yes, that's understood

Hanno Becker (Oct 04 2023 at 09:21):

But, ultimately, the position information is not passed through context here, but through the string itself -- which is difficult to notice because it's elided upon normal printing.

Fabian Huch (Oct 04 2023 at 09:30):

Yup. That is not obvious from the signature but when you read through the code it becomes clear:

fun read_type_name flags ctxt text =
  let
    val source = Syntax.read_input text;
    val (T, reports) = check_type_name flags ctxt (Input.source_content source);
    val _ = Context_Position.reports ctxt reports;

Hanno Becker (Oct 04 2023 at 09:31):

Do you happen to know if there are helper functions for removing such position annotations to get "plain string"?

Fabian Huch (Oct 04 2023 at 09:34):

Not by memory but there must be, look at the module where the type of source here is defined.

Hanno Becker (Oct 04 2023 at 09:36):

Syntax.read_input #> Input.string_of seems to work

Hanno Becker (Oct 04 2023 at 09:36):

Great, I think I can make progress now. Thanks for the help! :pray:

Last updated: May 04 2024 at 16:18 UTC