# HG changeset patch
# User wenzelm
# Date 1415784659 -3600
# Node ID 92b6f4e68c5a216181b70df7171c858b45e8ae8e
# Parent  51890cb80b305359491a21d536a76f2212e53ef9
more careful ML source positions, for improved PIDE markup;

diff -r 51890cb80b30 -r 92b6f4e68c5a src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 11 21:14:19 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Nov 12 10:30:59 2014 +0100
@@ -214,9 +214,10 @@
   fun ml_tactic source ctxt =
     let
       val ctxt' = ctxt |> Context.proof_map
-        (ML_Context.expression (#range source)
-          "fun tactic (ctxt : Proof.context) : tactic"
-          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
+        (ML_Context.expression (#range source) "tactic" "Proof.context -> tactic"
+          "Context.map_proof (ML_Tactic.set tactic)"
+          (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
+           ML_Lex.read_source false source));
     in Data.get ctxt' ctxt end;
 end;
 *}
diff -r 51890cb80b30 -r 92b6f4e68c5a src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Nov 12 10:30:59 2014 +0100
@@ -208,8 +208,7 @@
 
 fun attribute_setup name source comment =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val parser: Thm.attribute context_parser"
+  |> ML_Context.expression (#range source) "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 51890cb80b30 -r 92b6f4e68c5a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Nov 12 10:30:59 2014 +0100
@@ -60,14 +60,14 @@
 
 fun global_setup source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val setup: theory -> theory" "Context.map_theory setup"
+  |> ML_Context.expression (#range source) "setup" "theory -> theory"
+    "Context.map_theory setup"
   |> Context.theory_map;
 
 fun local_setup source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup"
+  |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
+    "Context.map_proof local_setup"
   |> Context.proof_map;
 
 
@@ -75,36 +75,36 @@
 
 fun parse_ast_translation source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
+  |> ML_Context.expression (#range source) "parse_ast_translation"
+    "(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 false source
-  |> ML_Context.expression (#range source)
-    "val parse_translation: (string * (Proof.context -> term list -> term)) list"
+  |> ML_Context.expression (#range source) "parse_translation"
+    "(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 false source
-  |> ML_Context.expression (#range source)
-    "val print_translation: (string * (Proof.context -> term list -> term)) list"
+  |> ML_Context.expression (#range source) "print_translation"
+    "(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 false source
-  |> ML_Context.expression (#range source)
-    "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
+  |> ML_Context.expression (#range source) "typed_print_translation"
+    "(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 false source
-  |> ML_Context.expression (#range source)
-    "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
+  |> ML_Context.expression (#range source) "print_ast_translation"
+    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   |> Context.theory_map;
 
@@ -160,8 +160,7 @@
 
 fun declaration {syntax, pervasive} source =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val declaration: Morphism.declaration"
+  |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
     ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
       \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   |> Context.proof_map;
@@ -171,8 +170,8 @@
 
 fun simproc_setup name lhss source identifier =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
+  |> ML_Context.expression (#range source) "proc"
+    "Morphism.morphism -> Proof.context -> cterm -> thm option"
     ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
       \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
       \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
diff -r 51890cb80b30 -r 92b6f4e68c5a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 12 10:30:59 2014 +0100
@@ -283,8 +283,10 @@
       let
         val context' = context |>
           ML_Context.expression (#range source)
-            "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
-            "Method.set_tactic tactic" (ML_Lex.read_source false source);
+            "tactic" "Morphism.morphism -> thm list -> tactic"
+            "Method.set_tactic tactic"
+            (ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
+             ML_Lex.read_source false source);
         val tac = the_tactic context';
       in
         fn phi =>
@@ -379,8 +381,8 @@
 
 fun method_setup name source comment =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source)
-    "val parser: (Proof.context -> Proof.method) context_parser"
+  |> ML_Context.expression (#range source) "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 51890cb80b30 -r 92b6f4e68c5a src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Nov 12 10:30:59 2014 +0100
@@ -32,10 +32,12 @@
       end;
 
     fun reported_entity kind loc decl =
-      let val pos = Exn_Properties.position_of loc in
-        is_reported pos ?
+      let
+        val pos = Exn_Properties.position_of loc;
+        val def_pos = Exn_Properties.position_of decl;
+      in
+        (is_reported pos andalso pos <> def_pos) ?
           let
-            val def_pos = Exn_Properties.position_of decl;
             fun markup () =
               (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
           in cons (pos, markup, fn () => "") end
diff -r 51890cb80b30 -r 92b6f4e68c5a src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Nov 11 21:14:19 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Nov 12 10:30:59 2014 +0100
@@ -25,7 +25,7 @@
   val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
     ML_Lex.token Antiquote.antiquote list -> unit
   val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
-  val expression: Position.range -> string -> string ->
+  val expression: Position.range -> string -> string -> string ->
     ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
 end
 
@@ -183,14 +183,15 @@
   Context.setmp_thread_data (Option.map Context.Proof ctxt)
     (fn () => eval_source flags source) ();
 
-fun expression range bind body ants =
+fun expression range name constraint body ants =
   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 "Context.set_thread_data (SOME (let val " @ visible name @
+        hidden (": " ^ constraint ^ " =") @ ants @
         hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
   end;