# HG changeset patch # User paulson # Date 1426000886 0 # Node ID 1c937d56a70a639b55f36efc0dd731fd61cfc819 # Parent 651ea265d56811ec3b7ed20be0ee282dcae52d0a# Parent 0e9f303d151524aca91b2a24d51be7aa6c6ad090 Merge diff -r 651ea265d568 -r 1c937d56a70a src/Pure/Isar/args.ML --- a/src/Pure/Isar/args.ML Tue Mar 10 15:20:40 2015 +0000 +++ b/src/Pure/Isar/args.ML Tue Mar 10 15:21:26 2015 +0000 @@ -59,6 +59,7 @@ val goal_spec: ((int -> tactic) -> tactic) context_parser val attribs: (xstring * Position.T -> string) -> Token.src list parser val opt_attribs: (xstring * Position.T -> string) -> Token.src list parser + val checked_name: (xstring * Position.T -> string) -> string parser end; structure Args: ARGS = @@ -209,4 +210,11 @@ fun opt_attribs check = Scan.optional (attribs check) []; + +(* checked name *) + +fun checked_name check = + let fun intern tok = check (Token.content_of tok, Token.pos_of tok); + in internal_name >> #1 || Parse.token Parse.xname >> evaluate Token.name0 intern end; + end; diff -r 651ea265d568 -r 1c937d56a70a src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Mar 10 15:20:40 2015 +0000 +++ b/src/Pure/Isar/method.ML Tue Mar 10 15:21:26 2015 +0000 @@ -75,8 +75,8 @@ val position: text_range option -> Position.T val reports_of: text_range -> Position.report list val report: text_range -> unit - val parse0: text_range parser val parse: text_range parser + val parse_internal: Proof.context -> text_range parser end; structure Method: METHOD = @@ -554,45 +554,58 @@ end; -(* outer parser *) +(* parser *) + +local fun is_symid_meth s = s <> "|" andalso s <> "?" andalso s <> "+" andalso Token.ident_or_symbolic s; -local +fun parser check_ctxt low_pri = + let + val (meth_name, mk_src) = + (case check_ctxt of + NONE => (Parse.xname, Token.src) + | SOME ctxt => + (Args.checked_name (fn (xname, _) => check_name ctxt (xname, Position.none)), + fn name => fn args => #1 (check_src ctxt (Token.src name args)))); -fun meth5 x = - (Parse.position Parse.xname >> (fn name => Source (Token.src name [])) || - Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => - Source (Token.src ("cartouche", Token.pos_of tok) [tok])) || - Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x -and meth4 x = - (meth5 -- Parse.position (Parse.$$$ "?") - >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || - meth5 -- Parse.position (Parse.$$$ "+") - >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || - meth5 -- - (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) - >> (fn (m, (((_, pos1), n), (_, pos2))) => - Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || - meth5) x -and meth3 x = - (Parse.position Parse.xname -- Parse.args1 is_symid_meth >> (Source o uncurry Token.src) || - meth4) x -and meth2 x = - (Parse.enum1_positions "," meth3 - >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x -and meth1 x = - (Parse.enum1_positions ";" meth2 - >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x -and meth0 x = - (Parse.enum1_positions "|" meth1 - >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; + fun meth5 x = + (Parse.position meth_name >> (fn name => Source (mk_src name [])) || + Scan.ahead Parse.cartouche |-- Parse.not_eof >> (fn tok => + Source (mk_src ("cartouche", Token.pos_of tok) [tok])) || + Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x + and meth4 x = + (meth5 -- Parse.position (Parse.$$$ "?") + >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Try, [m])) || + meth5 -- Parse.position (Parse.$$$ "+") + >> (fn (m, (_, pos)) => Combinator (combinator_info [pos], Repeat1, [m])) || + meth5 -- + (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]")) + >> (fn (m, (((_, pos1), n), (_, pos2))) => + Combinator (combinator_info [pos1, pos2], Select_Goals n, [m])) || + meth5) x + and meth3 x = + (Parse.position meth_name -- Parse.args1 is_symid_meth >> (Source o uncurry mk_src) || + meth4) x + and meth2 x = + (Parse.enum1_positions "," meth3 + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then, ms))) x + and meth1 x = + (Parse.enum1_positions ";" meth2 + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Then_All_New, ms))) x + and meth0 x = + (Parse.enum1_positions "|" meth1 + >> (fn ([m], _) => m | (ms, ps) => Combinator (combinator_info ps, Orelse, ms))) x; + in + Scan.trace (if low_pri then meth0 else meth4) + >> (fn (m, toks) => (m, Token.range_of toks)) + end; in -val parse0 = Scan.trace meth0 >> (fn (m, toks) => (m, Token.range_of toks)); -val parse = Scan.trace meth4 >> (fn (m, toks) => (m, Token.range_of toks)); +val parse = parser NONE false; +fun parse_internal ctxt = parser (SOME ctxt) true; end; diff -r 651ea265d568 -r 1c937d56a70a src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue Mar 10 15:20:40 2015 +0000 +++ b/src/Pure/Isar/token.ML Tue Mar 10 15:21:26 2015 +0000 @@ -206,13 +206,15 @@ if null args then pos else Position.set_range (pos, #2 (range_of args)); -fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) = - let - val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos); - val space = Name_Space.space_of_table table; - val kind = Name_Space.kind_of space; - val markup = Name_Space.markup space name; - in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end; +fun check_src _ table (src as Src {name = (name, _), output_info = SOME _, ...}) = + (src, Name_Space.get table name) + | check_src ctxt table (Src {name = (xname, pos), args, output_info = NONE}) = + let + val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos); + val space = Name_Space.space_of_table table; + val kind = Name_Space.kind_of space; + val markup = Name_Space.markup space name; + in (Src {name = (name, pos), args = args, output_info = SOME (kind, markup)}, x) end; (* stopper *)