# HG changeset patch
# User wenzelm
# Date 1415817056 -3600
# Node ID 87d4ce309e04b6ef1da6d519e8be33ff998c2b94
# Parent  b66788d19c0f0146b536cbab9237f42d1752419e# Parent  302104d8366b72e680aa8e859b16f9660ff80f06
merged

diff -r b66788d19c0f -r 87d4ce309e04 src/HOL/Tools/Function/fun_cases.ML
--- a/src/HOL/Tools/Function/fun_cases.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML	Wed Nov 12 19:30:56 2014 +0100
@@ -45,7 +45,7 @@
   let
     val thmss =
       map snd args
-      |> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
+      |> burrow (grouped 10 Par_List.map_independent (mk_fun_cases lthy o prep_prop lthy));
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
diff -r b66788d19c0f -r 87d4ce309e04 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Nov 12 19:30:56 2014 +0100
@@ -585,7 +585,7 @@
   let
     val thmss =
       map snd args
-      |> burrow (grouped 10 Par_List.map (mk_cases lthy o prep_prop lthy));
+      |> burrow (grouped 10 Par_List.map_independent (mk_cases lthy o prep_prop lthy));
     val facts =
       map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
         args thmss;
diff -r b66788d19c0f -r 87d4ce309e04 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Nov 12 19:30:56 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 b66788d19c0f -r 87d4ce309e04 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Wed Nov 12 19:30:56 2014 +0100
@@ -18,6 +18,7 @@
 sig
   val managed_results: string -> ('a -> 'b) -> 'a list -> 'b Exn.result list
   val map_name: string -> ('a -> 'b) -> 'a list -> 'b list
+  val map_independent: ('a -> 'b) -> 'a list -> 'b list
   val map: ('a -> 'b) -> 'a list -> 'b list
   val get_some: ('a -> 'b option) -> 'a list -> 'b option
   val find_some: ('a -> bool) -> 'a list -> 'a option
@@ -51,6 +52,7 @@
 
 fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
 fun map f = map_name "Par_List.map" f;
+fun map_independent f = map (Exn.interruptible_capture f) #> Par_Exn.release_all;
 
 fun get_some f xs =
   let
diff -r b66788d19c0f -r 87d4ce309e04 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Nov 12 19:30:56 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 b66788d19c0f -r 87d4ce309e04 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Nov 12 19:30:56 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 b66788d19c0f -r 87d4ce309e04 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 12 19:30:56 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 b66788d19c0f -r 87d4ce309e04 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Nov 12 19:30:56 2014 +0100
@@ -117,8 +117,7 @@
 
     val Asss =
       (map o map) snd raw_specss
-      |> (burrow o burrow)
-        (grouped 10 (Par_List.map_name "Specification.parse_prop") (parse_prop params_ctxt));
+      |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
     val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
       |> fold Name.declare xs;
     val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
diff -r b66788d19c0f -r 87d4ce309e04 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Nov 12 19:30:56 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 b66788d19c0f -r 87d4ce309e04 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Nov 12 19:30:56 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;
 
diff -r b66788d19c0f -r 87d4ce309e04 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 12 19:30:56 2014 +0100
@@ -273,13 +273,13 @@
 fun read_sort ctxt = parse_sort ctxt #> check_sort ctxt;
 
 fun read_typs ctxt =
-  grouped 10 (Par_List.map_name "Syntax.read_typs") (parse_typ ctxt) #> check_typs ctxt;
+  grouped 10 Par_List.map_independent (parse_typ ctxt) #> check_typs ctxt;
 
 fun read_terms ctxt =
-  grouped 10 (Par_List.map_name "Syntax.read_terms") (parse_term ctxt) #> check_terms ctxt;
+  grouped 10 Par_List.map_independent (parse_term ctxt) #> check_terms ctxt;
 
 fun read_props ctxt =
-  grouped 10 (Par_List.map_name "Syntax.read_props") (parse_prop ctxt) #> check_props ctxt;
+  grouped 10 Par_List.map_independent (parse_prop ctxt) #> check_props ctxt;
 
 val read_typ = singleton o read_typs;
 val read_term = singleton o read_terms;
diff -r b66788d19c0f -r 87d4ce309e04 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Nov 12 17:37:44 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Nov 12 19:30:56 2014 +0100
@@ -195,7 +195,7 @@
     val _ = Position.reports (maps words ants);
   in implode (map expand ants) end;
 
-fun check_text {delimited, text, range} state =
+fun check_text ({delimited, text, range}: Symbol_Pos.source) state =
  (Position.report (fst range) (Markup.language_document delimited);
   if Toplevel.is_skipped_proof state then ()
   else ignore (eval_antiquote state (text, fst range)));