# 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)));