# HG changeset patch
# User wenzelm
# Date 1415733098 -3600
# Node ID 162a4c2e97bc222b21c0281f4e3a6d0800ac27db
# Parent  e42da880c61ea1d88025b192bf2c386de548636b
more careful ML source positions, for improved PIDE markup;

diff -r e42da880c61e -r 162a4c2e97bc src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Nov 11 18:16:25 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Nov 11 20:11:38 2014 +0100
@@ -206,13 +206,12 @@
 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 cmt =
-  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-    ML_Lex.read_source false source @
-    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+fun attribute_setup name source comment =
+  ML_Lex.read_source false source
   |> ML_Context.expression (#range source)
-    "val (name, scan, comment): binding * attribute context_parser * string"
-    "Context.map_proof (Attrib.local_setup name scan comment)"
+    "val parser: Thm.attribute context_parser"
+    ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+      " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
 
 
diff -r e42da880c61e -r 162a4c2e97bc src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 18:16:25 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 20:11:38 2014 +0100
@@ -67,7 +67,7 @@
 fun local_setup source =
   ML_Lex.read_source false source
   |> ML_Context.expression (#range source)
-    "val setup: local_theory -> local_theory" "Context.map_proof setup"
+    "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup"
   |> Context.proof_map;
 
 
diff -r e42da880c61e -r 162a4c2e97bc src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Nov 11 18:16:25 2014 +0100
+++ b/src/Pure/Isar/method.ML	Tue Nov 11 20:11:38 2014 +0100
@@ -377,13 +377,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 cmt =
-  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-    ML_Lex.read_source false source @
-    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
+fun method_setup name source comment =
+  ML_Lex.read_source false source
   |> ML_Context.expression (#range source)
-    "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
-    "Context.map_proof (Method.local_setup name scan comment)"
+    "val parser: (Proof.context -> Proof.method) context_parser"
+    ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
+      " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
 
 
diff -r e42da880c61e -r 162a4c2e97bc src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Nov 11 18:16:25 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Nov 11 20:11:38 2014 +0100
@@ -184,11 +184,15 @@
     (fn () => eval_source flags source) ();
 
 fun expression range bind body ants =
-  exec (fn () =>
-    eval ML_Compiler.flags (#1 range)
-     (ML_Lex.read_set_range range ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @
-      ants @
-      ML_Lex.read_set_range range (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
+  let
+    val hidden = ML_Lex.read Position.none;
+    val visible = ML_Lex.read_set_range range;
+  in
+    exec (fn () =>
+      eval ML_Compiler.flags (#1 range)
+       (hidden "Context.set_thread_data (SOME (let" @ visible bind @ hidden "=" @ ants @
+        hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
+  end;
 
 end;