clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);

--- a/src/HOL/ex/Cartouche_Examples.thy	Thu Oct 25 17:08:04 2018 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy	Thu Oct 25 21:29:08 2018 +0200
@@ -176,7 +176,7 @@
   fun ml_tactic source ctxt =
     let
       val ctxt' = ctxt |> Context.proof_map
-        (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
+        (ML_Context.expression ("tactic", Position.thread_data ()) "Proof.context -> tactic"
           "Context.map_proof (ML_Tactic.set tactic)"
           (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
     in Data.get ctxt' ctxt end;

--- a/src/Pure/Isar/attrib.ML	Thu Oct 25 17:08:04 2018 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Oct 25 21:29:08 2018 +0200
@@ -214,10 +214,11 @@
 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
 
-fun attribute_setup name source comment =
+fun attribute_setup (name, pos) source comment =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
-    ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+  |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
+    ("Context.map_proof (Attrib.local_setup " ^
+      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
       " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
 

--- a/src/Pure/Isar/isar_cmd.ML	Thu Oct 25 17:08:04 2018 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Oct 25 21:29:08 2018 +0200
@@ -52,13 +52,13 @@
 
 fun setup source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
+  |> ML_Context.expression ("setup", Position.thread_data ()) "theory -> theory"
     "Context.map_theory setup"
   |> Context.theory_map;
 
 fun local_setup source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
+  |> ML_Context.expression ("local_setup", Position.thread_data ()) "local_theory -> local_theory"
     "Context.map_proof local_setup"
   |> Context.proof_map;
 
@@ -67,35 +67,35 @@
 
 fun parse_ast_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
+  |> ML_Context.expression ("parse_ast_translation", Position.thread_data ())
     "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
   |> Context.theory_map;
 
 fun parse_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "parse_translation"
+  |> ML_Context.expression ("parse_translation", Position.thread_data ())
     "(string * (Proof.context -> term list -> term)) list"
     "Context.map_theory (Sign.parse_translation parse_translation)"
   |> Context.theory_map;
 
 fun print_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "print_translation"
+  |> ML_Context.expression ("print_translation", Position.thread_data ())
     "(string * (Proof.context -> term list -> term)) list"
     "Context.map_theory (Sign.print_translation print_translation)"
   |> Context.theory_map;
 
 fun typed_print_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "typed_print_translation"
+  |> ML_Context.expression ("typed_print_translation", Position.thread_data ())
     "(string * (Proof.context -> typ -> term list -> term)) list"
     "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   |> Context.theory_map;
 
 fun print_ast_translation source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "print_ast_translation"
+  |> ML_Context.expression ("print_ast_translation", Position.thread_data ())
     "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   |> Context.theory_map;
@@ -143,7 +143,7 @@
 
 fun declaration {syntax, pervasive} source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
+  |> ML_Context.expression ("declaration", Position.thread_data ()) "Morphism.declaration"
     ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
       \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   |> Context.proof_map;
@@ -153,7 +153,7 @@
 
 fun simproc_setup name lhss source =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "proc"
+  |> ML_Context.expression ("proc", Position.thread_data ())
     "Morphism.morphism -> Proof.context -> cterm -> thm option"
     ("Context.map_proof (Simplifier.define_simproc_cmd " ^
       ML_Syntax.atomic (ML_Syntax.make_binding name) ^

--- a/src/Pure/Isar/method.ML	Thu Oct 25 17:08:04 2018 +0200
+++ b/src/Pure/Isar/method.ML	Thu Oct 25 21:29:08 2018 +0200
@@ -369,8 +369,8 @@
     Scan.lift (Args.text_declaration (fn source =>
       let
         val context' = context |>
-          ML_Context.expression (Input.range_of source)
-            "tactic" "Morphism.morphism -> thm list -> tactic"
+          ML_Context.expression ("tactic", Position.thread_data ())
+            "Morphism.morphism -> thm list -> tactic"
             "Method.set_tactic tactic"
             (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
              ML_Lex.read_source source);
@@ -475,11 +475,12 @@
 fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
 
-fun method_setup name source comment =
+fun method_setup (name, pos) source comment =
   ML_Lex.read_source source
-  |> ML_Context.expression (Input.range_of source) "parser"
+  |> ML_Context.expression ("parser", pos)
     "(Proof.context -> Proof.method) context_parser"
-    ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+    ("Context.map_proof (Method.local_setup " ^
+      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
       " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
 

--- a/src/Pure/ML/ml_context.ML	Thu Oct 25 17:08:04 2018 +0200
+++ b/src/Pure/ML/ml_context.ML	Thu Oct 25 21:29:08 2018 +0200
@@ -21,7 +21,7 @@
     ML_Lex.token Antiquote.antiquote list -> unit
   val eval_source_in: Proof.context option -> ML_Compiler.flags -> Input.source -> unit
   val exec: (unit -> unit) -> Context.generic -> Context.generic
-  val expression: Position.range -> string -> string -> string ->
+  val expression: string * Position.T -> string -> string ->
     ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
 end
 
@@ -214,10 +214,11 @@
     SOME context' => context'
   | NONE => error "Missing context after execution");
 
-fun expression range name constraint body ants =
+fun expression (name, pos) constraint body ants =
   exec (fn () =>
-    eval ML_Compiler.flags (#1 range)
-     (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
+    eval ML_Compiler.flags pos
+     (ML_Lex.read "Context.put_generic_context (SOME (let val " @
+       ML_Lex.read_set_range (Position.range_of_properties (Position.properties_of pos)) name @
       ML_Lex.read (": " ^ constraint ^ " =") @ ants @
       ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));