clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
authorwenzelm
Thu Oct 25 21:29:08 2018 +0200 (7 months ago ago)
changeset 69188d8849cfad60f
parent 69187 573b7fbd96a8
child 69189 2fd73a1a0937
clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Thu Oct 25 17:08:04 2018 +0200
     1.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Oct 25 21:29:08 2018 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4    fun ml_tactic source ctxt =
     1.5      let
     1.6        val ctxt' = ctxt |> Context.proof_map
     1.7 -        (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
     1.8 +        (ML_Context.expression ("tactic", Position.thread_data ()) "Proof.context -> tactic"
     1.9            "Context.map_proof (ML_Tactic.set tactic)"
    1.10            (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
    1.11      in Data.get ctxt' ctxt end;
     2.1 --- a/src/Pure/Isar/attrib.ML	Thu Oct 25 17:08:04 2018 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Thu Oct 25 21:29:08 2018 +0200
     2.3 @@ -214,10 +214,11 @@
     2.4  fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
     2.5  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
     2.6  
     2.7 -fun attribute_setup name source comment =
     2.8 +fun attribute_setup (name, pos) source comment =
     2.9    ML_Lex.read_source source
    2.10 -  |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
    2.11 -    ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    2.12 +  |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
    2.13 +    ("Context.map_proof (Attrib.local_setup " ^
    2.14 +      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
    2.15        " parser " ^ ML_Syntax.print_string comment ^ ")")
    2.16    |> Context.proof_map;
    2.17  
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 25 17:08:04 2018 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 25 21:29:08 2018 +0200
     3.3 @@ -52,13 +52,13 @@
     3.4  
     3.5  fun setup source =
     3.6    ML_Lex.read_source source
     3.7 -  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
     3.8 +  |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
     3.9      "Context.map_theory setup"
    3.10    |> Context.theory_map;
    3.11  
    3.12  fun local_setup source =
    3.13    ML_Lex.read_source source
    3.14 -  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
    3.15 +  |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
    3.16      "Context.map_proof local_setup"
    3.17    |> Context.proof_map;
    3.18  
    3.19 @@ -67,35 +67,35 @@
    3.20  
    3.21  fun parse_ast_translation source =
    3.22    ML_Lex.read_source source
    3.23 -  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
    3.24 +  |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
    3.25      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    3.26      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    3.27    |> Context.theory_map;
    3.28  
    3.29  fun parse_translation source =
    3.30    ML_Lex.read_source source
    3.31 -  |> ML_Context.expression (Input.range_of source) "parse_translation"
    3.32 +  |> ML_Context.expression ("parse_translation", Position.thread_data ())
    3.33      "(string * (Proof.context -> term list -> term)) list"
    3.34      "Context.map_theory (Sign.parse_translation parse_translation)"
    3.35    |> Context.theory_map;
    3.36  
    3.37  fun print_translation source =
    3.38    ML_Lex.read_source source
    3.39 -  |> ML_Context.expression (Input.range_of source) "print_translation"
    3.40 +  |> ML_Context.expression ("print_translation", Position.thread_data ())
    3.41      "(string * (Proof.context -> term list -> term)) list"
    3.42      "Context.map_theory (Sign.print_translation print_translation)"
    3.43    |> Context.theory_map;
    3.44  
    3.45  fun typed_print_translation source =
    3.46    ML_Lex.read_source source
    3.47 -  |> ML_Context.expression (Input.range_of source) "typed_print_translation"
    3.48 +  |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
    3.49      "(string * (Proof.context -> typ -> term list -> term)) list"
    3.50      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    3.51    |> Context.theory_map;
    3.52  
    3.53  fun print_ast_translation source =
    3.54    ML_Lex.read_source source
    3.55 -  |> ML_Context.expression (Input.range_of source) "print_ast_translation"
    3.56 +  |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
    3.57      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    3.58      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    3.59    |> Context.theory_map;
    3.60 @@ -143,7 +143,7 @@
    3.61  
    3.62  fun declaration {syntax, pervasive} source =
    3.63    ML_Lex.read_source source
    3.64 -  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
    3.65 +  |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
    3.66      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    3.67        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    3.68    |> Context.proof_map;
    3.69 @@ -153,7 +153,7 @@
    3.70  
    3.71  fun simproc_setup name lhss source =
    3.72    ML_Lex.read_source source
    3.73 -  |> ML_Context.expression (Input.range_of source) "proc"
    3.74 +  |> ML_Context.expression ("proc", Position.thread_data ())
    3.75      "Morphism.morphism -> Proof.context -> cterm -> thm option"
    3.76      ("Context.map_proof (Simplifier.define_simproc_cmd " ^
    3.77        ML_Syntax.atomic (ML_Syntax.make_binding name) ^
     4.1 --- a/src/Pure/Isar/method.ML	Thu Oct 25 17:08:04 2018 +0200
     4.2 +++ b/src/Pure/Isar/method.ML	Thu Oct 25 21:29:08 2018 +0200
     4.3 @@ -369,8 +369,8 @@
     4.4      Scan.lift (Args.text_declaration (fn source =>
     4.5        let
     4.6          val context' = context |>
     4.7 -          ML_Context.expression (Input.range_of source)
     4.8 -            "tactic" "Morphism.morphism -> thm list -> tactic"
     4.9 +          ML_Context.expression ("tactic", Position.thread_data ())
    4.10 +            "Morphism.morphism -> thm list -> tactic"
    4.11              "Method.set_tactic tactic"
    4.12              (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
    4.13               ML_Lex.read_source source);
    4.14 @@ -475,11 +475,12 @@
    4.15  fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
    4.16  fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
    4.17  
    4.18 -fun method_setup name source comment =
    4.19 +fun method_setup (name, pos) source comment =
    4.20    ML_Lex.read_source source
    4.21 -  |> ML_Context.expression (Input.range_of source) "parser"
    4.22 +  |> ML_Context.expression ("parser", pos)
    4.23      "(Proof.context -> Proof.method) context_parser"
    4.24 -    ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    4.25 +    ("Context.map_proof (Method.local_setup " ^
    4.26 +      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
    4.27        " parser " ^ ML_Syntax.print_string comment ^ ")")
    4.28    |> Context.proof_map;
    4.29  
     5.1 --- a/src/Pure/ML/ml_context.ML	Thu Oct 25 17:08:04 2018 +0200
     5.2 +++ b/src/Pure/ML/ml_context.ML	Thu Oct 25 21:29:08 2018 +0200
     5.3 @@ -21,7 +21,7 @@
     5.4      ML_Lex.token Antiquote.antiquote list -> unit
     5.5    val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
     5.6    val exec: (unit -> unit) -> Context.generic -> Context.generic
     5.7 -  val expression: Position.range -> string -> string -> string ->
     5.8 +  val expression: string * Position.T -> string -> string ->
     5.9      ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
    5.10  end
    5.11  
    5.12 @@ -214,10 +214,11 @@
    5.13      SOME context' => context'
    5.14    | NONE => error "Missing context after execution");
    5.15  
    5.16 -fun expression range name constraint body ants =
    5.17 +fun expression (name, pos) constraint body ants =
    5.18    exec (fn () =>
    5.19 -    eval ML_Compiler.flags (#1 range)
    5.20 -     (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
    5.21 +    eval ML_Compiler.flags pos
    5.22 +     (ML_Lex.read "Context.put_generic_context (SOME (let val " @
    5.23 +       ML_Lex.read_set_range (Position.range_of_properties (Position.properties_of pos)) name @
    5.24        ML_Lex.read (": " ^ constraint ^ " =") @ ants @
    5.25        ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
    5.26