--- 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;
--- 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;
--- 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;
*}
--- 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
--- 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;
--- 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 ^ "})")
--- 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;
--- 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);
--- 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
--- 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;
--- 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;
--- 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)));