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