# HG changeset patch # User wenzelm # Date 1409144133 -7200 # Node ID 930727de976c3656b1df3d5a73bf7e1092887b61 # Parent b5cdfb352814072081b9097c457d73dacc149502# Parent aa6296d09e0eaef6d99dba5d4e4eabf26a901574 merged diff -r b5cdfb352814 -r 930727de976c src/HOL/Tools/recdef.ML --- 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; diff -r b5cdfb352814 -r 930727de976c src/Provers/clasimp.ML --- 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 @ diff -r b5cdfb352814 -r 930727de976c src/Provers/classical.ML --- 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); diff -r b5cdfb352814 -r 930727de976c src/Provers/splitter.ML --- 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 *) diff -r b5cdfb352814 -r 930727de976c src/Pure/General/symbol_pos.ML --- 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; diff -r b5cdfb352814 -r 930727de976c src/Pure/Isar/attrib.ML --- 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) => diff -r b5cdfb352814 -r 930727de976c src/Pure/Isar/method.ML --- 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; diff -r b5cdfb352814 -r 930727de976c src/Pure/Isar/token.ML --- 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; diff -r b5cdfb352814 -r 930727de976c src/Pure/ML/ml_antiquotations.ML --- 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 diff -r b5cdfb352814 -r 930727de976c src/Pure/ML/ml_thms.ML --- 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); diff -r b5cdfb352814 -r 930727de976c src/Pure/PIDE/markup.ML --- 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 *) diff -r b5cdfb352814 -r 930727de976c src/Pure/PIDE/markup.scala --- 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" diff -r b5cdfb352814 -r 930727de976c src/Pure/Syntax/syntax.ML --- 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, _), _)] => diff -r b5cdfb352814 -r 930727de976c src/Pure/Syntax/syntax_phases.ML --- 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; diff -r b5cdfb352814 -r 930727de976c src/Pure/simplifier.ML --- 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 = diff -r b5cdfb352814 -r 930727de976c src/Sequents/prover.ML --- 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); diff -r b5cdfb352814 -r 930727de976c src/Tools/intuitionistic.ML --- 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 diff -r b5cdfb352814 -r 930727de976c src/Tools/jEdit/src/rendering.scala --- 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) diff -r b5cdfb352814 -r 930727de976c src/ZF/Tools/typechk.ML --- 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";