--- a/src/HOL/Tools/recdef.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/HOL/Tools/recdef.ML Wed Aug 27 14:55:33 2014 +0200
@@ -143,15 +143,15 @@
val recdef_wfN = "recdef_wf";
val recdef_modifiers =
- [Args.$$$ recdef_simpN -- Args.colon >> K ((I, simp_add): Method.modifier),
- Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (I, simp_add),
- Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (I, simp_del),
- Args.$$$ recdef_congN -- Args.colon >> K (I, cong_add),
- Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (I, cong_add),
- Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (I, cong_del),
- Args.$$$ recdef_wfN -- Args.colon >> K (I, wf_add),
- Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (I, wf_add),
- Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (I, wf_del)] @
+ [Args.$$$ recdef_simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.$$$ recdef_simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.$$$ recdef_simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+ Args.$$$ recdef_congN -- Args.colon >> K (Method.modifier cong_add @{here}),
+ Args.$$$ recdef_congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
+ Args.$$$ recdef_congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here}),
+ Args.$$$ recdef_wfN -- Args.colon >> K (Method.modifier wf_add @{here}),
+ Args.$$$ recdef_wfN -- Args.add -- Args.colon >> K (Method.modifier wf_add @{here}),
+ Args.$$$ recdef_wfN -- Args.del -- Args.colon >> K (Method.modifier wf_del @{here})] @
Clasimp.clasimp_modifiers;
--- a/src/Provers/clasimp.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Provers/clasimp.ML Wed Aug 27 14:55:33 2014 +0200
@@ -191,9 +191,9 @@
val iffN = "iff";
val iff_modifiers =
- [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K ((I, iff_add): Method.modifier),
- Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (I, iff_add'),
- Args.$$$ iffN -- Args.del -- Args.colon >> K (I, iff_del)];
+ [Args.$$$ iffN -- Scan.option Args.add -- Args.colon >> K (Method.modifier iff_add @{here}),
+ Args.$$$ iffN -- Scan.option Args.add -- Args.query_colon >> K (Method.modifier iff_add' @{here}),
+ Args.$$$ iffN -- Args.del -- Args.colon >> K (Method.modifier iff_del @{here})];
val clasimp_modifiers =
Simplifier.simp_modifiers @ Splitter.split_modifiers @
--- a/src/Provers/classical.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Provers/classical.ML Wed Aug 27 14:55:33 2014 +0200
@@ -928,13 +928,13 @@
(* automatic methods *)
val cla_modifiers =
- [Args.$$$ destN -- Args.bang_colon >> K ((I, safe_dest NONE): Method.modifier),
- Args.$$$ destN -- Args.colon >> K (I, haz_dest NONE),
- Args.$$$ elimN -- Args.bang_colon >> K (I, safe_elim NONE),
- Args.$$$ elimN -- Args.colon >> K (I, haz_elim NONE),
- Args.$$$ introN -- Args.bang_colon >> K (I, safe_intro NONE),
- Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
- Args.del -- Args.colon >> K (I, rule_del)];
+ [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}),
+ Args.$$$ destN -- Args.colon >> K (Method.modifier (haz_dest NONE) @{here}),
+ Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}),
+ Args.$$$ elimN -- Args.colon >> K (Method.modifier (haz_elim NONE) @{here}),
+ Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}),
+ Args.$$$ introN -- Args.colon >> K (Method.modifier (haz_intro NONE) @{here}),
+ Args.del -- Args.colon >> K (Method.modifier rule_del @{here})];
fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
--- a/src/Provers/splitter.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Provers/splitter.ML Wed Aug 27 14:55:33 2014 +0200
@@ -457,9 +457,9 @@
(* methods *)
val split_modifiers =
- [Args.$$$ splitN -- Args.colon >> K ((I, split_add): Method.modifier),
- Args.$$$ splitN -- Args.add -- Args.colon >> K (I, split_add),
- Args.$$$ splitN -- Args.del -- Args.colon >> K (I, split_del)];
+ [Args.$$$ splitN -- Args.colon >> K (Method.modifier split_add @{here}),
+ Args.$$$ splitN -- Args.add -- Args.colon >> K (Method.modifier split_add @{here}),
+ Args.$$$ splitN -- Args.del -- Args.colon >> K (Method.modifier split_del @{here})];
(* theory setup *)
--- a/src/Pure/General/symbol_pos.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/General/symbol_pos.ML Wed Aug 27 14:55:33 2014 +0200
@@ -41,6 +41,7 @@
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
type source = {delimited: bool, text: text, pos: Position.T}
+ val source_explode: source -> T list
val source_content: source -> string * Position.T
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
@@ -261,6 +262,8 @@
type source = {delimited: bool, text: text, pos: Position.T};
+fun source_explode {delimited = _, text, pos} = explode (text, pos);
+
fun source_content {delimited = _, text, pos} =
let val syms = explode (text, pos) in (content syms, pos) end;
--- a/src/Pure/Isar/attrib.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 27 14:55:33 2014 +0200
@@ -48,6 +48,8 @@
val thm: thm context_parser
val thms: thm list context_parser
val multi_thm: thm list context_parser
+ val check_attribs: Proof.context -> Token.src list -> Token.src list
+ val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
val transform_facts: morphism ->
(Attrib.binding * (thm list * Token.src list) list) list ->
(Attrib.binding * (thm list * Token.src list) list) list
@@ -276,6 +278,25 @@
end;
+(* read attribute source *)
+
+fun check_attribs ctxt raw_srcs =
+ let
+ val srcs = map (check_src ctxt) raw_srcs;
+ val _ = map (attribute ctxt) srcs;
+ in srcs end;
+
+fun read_attribs ctxt source =
+ let
+ val syms = Symbol_Pos.source_explode source;
+ val lex = #1 (Keyword.get_lexicons ());
+ in
+ (case Token.read lex Parse.attribs (syms, #pos source) of
+ [raw_srcs] => check_attribs ctxt raw_srcs
+ | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
+ end;
+
+
(* transform fact expressions *)
fun transform_facts phi = map (fn ((a, atts), bs) =>
--- a/src/Pure/Isar/method.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Isar/method.ML Wed Aug 27 14:55:33 2014 +0200
@@ -67,7 +67,8 @@
val method_closure: Proof.context -> Token.src -> Token.src
val method_cmd: Proof.context -> Token.src -> Proof.context -> method
val evaluate: text -> Proof.context -> method
- type modifier = (Proof.context -> Proof.context) * attribute
+ type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
+ val modifier: attribute -> Position.T -> modifier
val section: modifier parser list -> declaration context_parser
val sections: modifier parser list -> declaration list context_parser
type text_range = text * Position.range
@@ -448,13 +449,19 @@
(** concrete syntax **)
-(* sections *)
+(* type modifier *)
+
+type modifier =
+ {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T};
-type modifier = (Proof.context -> Proof.context) * attribute;
+fun modifier attribute pos : modifier = {init = I, attribute = attribute, pos = pos};
+
+
+(* sections *)
local
-fun sect modifier = Scan.depend (fn context =>
+fun sect (modifier : modifier parser) = Scan.depend (fn context =>
let
val ctxt = Context.proof_of context;
fun prep_att src =
@@ -466,7 +473,7 @@
Parse.xthm >> (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs));
in
Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier parse_thm) >>
- (fn ((tok, (init, att)), thms) =>
+ (fn ((tok, {init, attribute, pos}), thms) =>
let
val decl =
(case Token.get_value tok of
@@ -475,7 +482,11 @@
let
val facts =
Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
- |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K att)]), bs));
+ |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
+ val _ =
+ Context_Position.report ctxt (Token.pos_of tok)
+ (Markup.entity Markup.method_modifierN ""
+ |> Markup.properties (Position.def_properties_of pos));
fun decl phi =
Context.mapping I init #>
Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
--- a/src/Pure/Isar/token.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Isar/token.ML Wed Aug 27 14:55:33 2014 +0200
@@ -86,9 +86,10 @@
val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) ->
Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
(Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
- val read_antiq: Scan.lexicon -> (T list -> 'a * T list) -> Symbol_Pos.T list * Position.T -> 'a
type 'a parser = T list -> 'a * T list
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
+ val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a list
+ val read_antiq: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
end;
@@ -585,28 +586,33 @@
end;
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
- let
- fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
- "@{" ^ Symbol_Pos.content syms ^ "}");
-
- val res =
- Source.of_list syms
- |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
- |> source_proper
- |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
- |> Source.exhaust;
- in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-
(** parsers **)
type 'a parser = T list -> 'a * T list;
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
+
+(* read source *)
+
+fun read lex scan (syms, pos) =
+ Source.of_list syms
+ |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
+ |> source_proper
+ |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE
+ |> Source.exhaust;
+
+fun read_antiq lex scan (syms, pos) =
+ let
+ fun err msg =
+ cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
+ "@{" ^ Symbol_Pos.content syms ^ "}");
+ val res = read lex scan (syms, pos) handle ERROR msg => err msg;
+ in (case res of [x] => x | _ => err "") end;
+
+
+(* wrapped syntax *)
+
fun syntax_generic scan (Src {name = (name, pos), args = args0, output_info}) context =
let
val args1 = map init_assignable args0;
--- a/src/Pure/ML/ml_antiquotations.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Wed Aug 27 14:55:33 2014 +0200
@@ -52,6 +52,16 @@
ML_Syntax.atomic (ML_Syntax.print_term t))));
+(* embedded source *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.value @{binding source}
+ (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
+ "{delimited = " ^ Bool.toString delimited ^
+ ", text = " ^ ML_Syntax.print_string text ^
+ ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
+
+
(* ML support *)
val _ = Theory.setup
--- a/src/Pure/ML/ml_thms.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/ML/ml_thms.ML Wed Aug 27 14:55:33 2014 +0200
@@ -44,10 +44,10 @@
(fn _ => fn raw_srcs => fn ctxt =>
let
val i = serial ();
- val srcs = map (Attrib.check_src ctxt) raw_srcs;
- val _ = map (Attrib.attribute ctxt) srcs;
+
val (a, ctxt') = ctxt
- |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs);
+ |> ML_Antiquotation.variant "attributes"
+ ||> put_attributes (i, Attrib.check_attribs ctxt raw_srcs);
val ml =
("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^
string_of_int i ^ ";\n", "Isabelle." ^ a);
--- a/src/Pure/PIDE/markup.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Aug 27 14:55:33 2014 +0200
@@ -72,6 +72,7 @@
val fixedN: string val fixed: string -> T
val caseN: string val case_: string -> T
val dynamic_factN: string val dynamic_fact: string -> T
+ val method_modifierN: string
val tfreeN: string val tfree: T
val tvarN: string val tvar: T
val freeN: string val free: T
@@ -365,7 +366,7 @@
val (hiddenN, hidden) = markup_elem "hidden";
-(* formal entities *)
+(* misc entities *)
val system_optionN = "system_option";
@@ -378,6 +379,8 @@
val (caseN, case_) = markup_string "case" nameN;
val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
+val method_modifierN = "method_modifier";
+
(* inner syntax *)
--- a/src/Pure/PIDE/markup.scala Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Aug 27 14:55:33 2014 +0200
@@ -169,7 +169,7 @@
val HIDDEN = "hidden"
- /* logical entities */
+ /* misc entities */
val CLASS = "class"
val TYPE_NAME = "type_name"
--- a/src/Pure/Syntax/syntax.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Aug 27 14:55:33 2014 +0200
@@ -185,10 +185,10 @@
let
fun parse_tree tree =
let
- val {delimited, text, pos} = token_source tree;
- val syms = Symbol_Pos.explode (text, pos);
- val _ = Context_Position.report ctxt pos (markup delimited);
- in parse (syms, pos) end;
+ val source = token_source tree;
+ val syms = Symbol_Pos.source_explode source;
+ val _ = Context_Position.report ctxt (#pos source) (markup (#delimited source));
+ in parse (syms, #pos source) end;
in
(case YXML.parse_body str handle Fail msg => error msg of
body as [tree as XML.Elem ((name, _), _)] =>
--- a/src/Pure/Syntax/syntax_phases.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Aug 27 14:55:33 2014 +0200
@@ -461,11 +461,11 @@
else decode_appl ps asts
| decode ps (Ast.Appl asts) = decode_appl ps asts;
- val {text, pos, ...} = Syntax.read_token str;
- val syms = Symbol_Pos.explode (text, pos);
+ val source = Syntax.read_token str;
+ val syms = Symbol_Pos.source_explode source;
val ast =
- parse_asts ctxt true root (syms, pos)
- |> uncurry (report_result ctxt pos)
+ parse_asts ctxt true root (syms, #pos source)
+ |> uncurry (report_result ctxt (#pos source))
|> decode [];
val _ = Context_Position.reports_text ctxt (! reports);
in ast end;
--- a/src/Pure/simplifier.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Pure/simplifier.ML Wed Aug 27 14:55:33 2014 +0200
@@ -332,21 +332,23 @@
(** method syntax **)
val cong_modifiers =
- [Args.$$$ congN -- Args.colon >> K ((I, cong_add): Method.modifier),
- Args.$$$ congN -- Args.add -- Args.colon >> K (I, cong_add),
- Args.$$$ congN -- Args.del -- Args.colon >> K (I, cong_del)];
+ [Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add @{here}),
+ Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add @{here}),
+ Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del @{here})];
val simp_modifiers =
- [Args.$$$ simpN -- Args.colon >> K (I, simp_add),
- Args.$$$ simpN -- Args.add -- Args.colon >> K (I, simp_add),
- Args.$$$ simpN -- Args.del -- Args.colon >> K (I, simp_del),
- Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
+ [Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+ Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >>
+ K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
@ cong_modifiers;
val simp_modifiers' =
- [Args.add -- Args.colon >> K (I, simp_add),
- Args.del -- Args.colon >> K (I, simp_del),
- Args.$$$ onlyN -- Args.colon >> K (Raw_Simplifier.clear_simpset, simp_add)]
+ [Args.add -- Args.colon >> K (Method.modifier simp_add @{here}),
+ Args.del -- Args.colon >> K (Method.modifier simp_del @{here}),
+ Args.$$$ onlyN -- Args.colon >>
+ K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = @{here}}]
@ cong_modifiers;
val simp_options =
--- a/src/Sequents/prover.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Sequents/prover.ML Wed Aug 27 14:55:33 2014 +0200
@@ -106,8 +106,8 @@
fun method tac =
Method.sections
- [Args.$$$ "add" -- Args.bang_colon >> K (I, safe_add),
- Args.$$$ "add" -- Args.colon >> K (I, unsafe_add)]
+ [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add @{here}),
+ Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add @{here})]
>> K (SIMPLE_METHOD' o tac);
--- a/src/Tools/intuitionistic.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Tools/intuitionistic.ML Wed Aug 27 14:55:33 2014 +0200
@@ -73,18 +73,18 @@
val elimN = "elim";
val destN = "dest";
-fun modifier name kind kind' att =
+fun modifier name kind kind' att pos =
Args.$$$ name |-- (kind >> K NONE || kind' |-- Parse.nat --| Args.colon >> SOME)
- >> (pair (I: Proof.context -> Proof.context) o att);
+ >> (fn arg => Method.modifier (att arg) pos);
val modifiers =
- [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
- modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
- modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
- modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
- modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
- modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
- Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
+ [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang @{here},
+ modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest @{here},
+ modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang @{here},
+ modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim @{here},
+ modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang @{here},
+ modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro @{here},
+ Args.del -- Args.colon >> K (Method.modifier Context_Rules.rule_del @{here})];
in
--- a/src/Tools/jEdit/src/rendering.scala Wed Aug 27 13:05:59 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Wed Aug 27 14:55:33 2014 +0200
@@ -480,7 +480,9 @@
Some(Text.Info(r, (t1 + t2, info)))
case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
val kind1 = Word.implode(Word.explode('_', kind))
- val txt1 = kind1 + " " + quote(name)
+ val txt1 =
+ if (name == "") kind1
+ else kind1 + " " + quote(name)
val t = prev.info._1
val txt2 =
if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
--- a/src/ZF/Tools/typechk.ML Wed Aug 27 13:05:59 2014 +0200
+++ b/src/ZF/Tools/typechk.ML Wed Aug 27 14:55:33 2014 +0200
@@ -115,8 +115,8 @@
val typecheck_setup =
Method.setup @{binding typecheck}
(Method.sections
- [Args.add -- Args.colon >> K (I, TC_add),
- Args.del -- Args.colon >> K (I, TC_del)]
+ [Args.add -- Args.colon >> K (Method.modifier TC_add @{here}),
+ Args.del -- Args.colon >> K (Method.modifier TC_del @{here})]
>> K (fn ctxt => SIMPLE_METHOD (CHANGED (typecheck_tac ctxt))))
"ZF type-checking";