# HG changeset patch # User wenzelm # Date 1353962764 -3600 # Node ID fb579401dc261b167da4d8585bae219d457c97e1 # Parent 98d35a7368bdb9ea4697b22e48bc245dc04cf2ec tuned signature; tuned; diff -r 98d35a7368bd -r fb579401dc26 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Doc/antiquote_setup.ML Mon Nov 26 21:46:04 2012 +0100 @@ -80,7 +80,7 @@ if txt2 = "" then txt1 else if kind = "type" then txt1 ^ " = " ^ txt2 else if kind = "exception" then txt1 ^ " of " ^ txt2 - else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1)) + else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2 else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Mon Nov 26 21:46:04 2012 +0100 @@ -126,7 +126,7 @@ val unyxml = XML.content_of o YXML.parse_body -val is_long_identifier = forall Lexicon.is_identifier o Long_Name.explode +val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode fun maybe_quote y = let val s = unyxml y in y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Nov 26 21:46:04 2012 +0100 @@ -232,7 +232,7 @@ let val s' = Long_Name.base_name s in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @ - [if Lexicon.is_identifier s' then s' else "x"]) + [if Symbol_Pos.is_identifier s' then s' else "x"]) end | name_of_typ _ = ""; diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Mon Nov 26 21:46:04 2012 +0100 @@ -46,7 +46,7 @@ fun type_name (TFree (name, _)) = unprefix "'" name | type_name (Type (name, _)) = let val name' = Long_Name.base_name name - in if Lexicon.is_identifier name' then name' else "x" end; + in if Symbol_Pos.is_identifier name' then name' else "x" end; in indexify_names (map type_name Ts) end; diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Nov 26 21:46:04 2012 +0100 @@ -61,7 +61,7 @@ fun needs_quoting reserved s = Symtab.defined reserved s orelse - exists (not o Lexicon.is_identifier) (Long_Name.explode s) + exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s) fun make_name reserved multi j name = (name |> needs_quoting reserved name ? quote) ^ diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Nov 26 21:46:04 2012 +0100 @@ -224,7 +224,7 @@ "using " ^ space_implode " " (map string_for_label ls) ^ " " fun command_call name [] = - name |> not (Lexicon.is_identifier name) ? enclose "(" ")" + name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = diff -r 98d35a7368bd -r fb579401dc26 src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/HOL/Tools/choice_specification.ML Mon Nov 26 21:46:04 2012 +0100 @@ -166,7 +166,7 @@ let val T = type_of c val cname = Long_Name.base_name (fst (dest_Const c)) - val vname = if Lexicon.is_identifier cname + val vname = if Symbol_Pos.is_identifier cname then cname else "x" in diff -r 98d35a7368bd -r fb579401dc26 src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/General/binding.ML Mon Nov 26 21:46:04 2012 +0100 @@ -136,7 +136,7 @@ fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding); fun check binding = - if Symbol.is_ident (Symbol.explode (name_of binding)) then () + if Symbol_Pos.is_identifier (name_of binding) then () else legacy_feature (bad binding); end; diff -r 98d35a7368bd -r fb579401dc26 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/General/symbol.ML Mon Nov 26 21:46:04 2012 +0100 @@ -53,7 +53,6 @@ val is_block_ctrl: symbol -> bool val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool - val is_ident: symbol list -> bool val beginning: int -> symbol list -> string val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source val explode: string -> symbol list @@ -512,12 +511,6 @@ |> implode; -(* identifiers *) - -fun is_ident [] = false - | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs; - - (* bump string -- treat as base 26 or base 1 numbers *) fun symbolic_end (_ :: "\\<^isub>" :: _) = true diff -r 98d35a7368bd -r fb579401dc26 src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/General/symbol_pos.ML Mon Nov 26 21:46:04 2012 +0100 @@ -37,6 +37,9 @@ val range: T list -> Position.range val implode_range: Position.T -> Position.T -> T list -> text * Position.range val explode: text * Position.T -> T list + val scan_ident: T list -> T list * T list + val is_ident: T list -> bool + val is_identifier: string -> bool end; structure Symbol_Pos: SYMBOL_POS = @@ -208,6 +211,18 @@ (Symbol.explode str) ([], Position.reset_range pos); in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end; + +(* identifiers *) + +val scan_ident = + Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol); + +fun is_ident [] = false + | is_ident (s :: ss) = Symbol.is_letter (symbol s) andalso forall (Symbol.is_letdig o symbol) ss; + +fun is_identifier s = + Symbol.is_ascii_identifier s orelse is_ident (explode (s, Position.none)); + end; structure Basic_Symbol_Pos = (*not open by default*) diff -r 98d35a7368bd -r fb579401dc26 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/Isar/proof_context.ML Mon Nov 26 21:46:04 2012 +0100 @@ -974,7 +974,7 @@ fold_map (fn (b, raw_T, mx) => fn ctxt => let val x = Variable.check_name b; - val _ = Lexicon.is_identifier (no_skolem internal x) orelse + val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse error ("Illegal variable name: " ^ Binding.print b); fun cond_tvars T = diff -r 98d35a7368bd -r fb579401dc26 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/Isar/token.ML Mon Nov 26 21:46:04 2012 +0100 @@ -311,7 +311,7 @@ fun ident_or_symbolic "begin" = false | ident_or_symbolic ":" = true | ident_or_symbolic "::" = true - | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s; + | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s; (* scan verbatim text *) diff -r 98d35a7368bd -r fb579401dc26 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/Syntax/lexicon.ML Mon Nov 26 21:46:04 2012 +0100 @@ -12,9 +12,6 @@ val free: string -> term val var: indexname -> term end - val is_identifier: string -> bool - val is_xid: string -> bool - val is_tid: string -> bool val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list @@ -25,6 +22,7 @@ val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list + val is_tid: string -> bool datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF @@ -90,32 +88,13 @@ -(** is_identifier etc. **) - -val is_identifier = Symbol.is_ident o Symbol.explode; - -fun is_xid s = - (case Symbol.explode s of - "_" :: cs => Symbol.is_ident cs - | cs => Symbol.is_ident cs); - -fun is_tid s = - (case Symbol.explode s of - "'" :: cs => Symbol.is_ident cs - | _ => false); - - - (** basic scanners **) open Basic_Symbol_Pos; fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg); -val scan_id = - Scan.one (Symbol.is_letter o Symbol_Pos.symbol) ::: - Scan.many (Symbol.is_letdig o Symbol_Pos.symbol); - +val scan_id = Symbol_Pos.scan_ident; val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat); val scan_tid = $$$ "'" @@@ scan_id; @@ -130,6 +109,11 @@ val scan_var = $$$ "?" @@@ scan_id_nat; val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat; +fun is_tid s = + (case try (unprefix "'") s of + SOME s' => Symbol_Pos.is_identifier s' + | NONE => false); + (** datatype token **) @@ -315,7 +299,8 @@ if Symbol.is_digit c then chop_idx cs (c :: ds) else idxname (c :: cs) ds; - val scan = (scan_id >> map Symbol_Pos.symbol) -- + val scan = + (scan_id >> map Symbol_Pos.symbol) -- Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1; in scan >> diff -r 98d35a7368bd -r fb579401dc26 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/Pure/tactic.ML Mon Nov 26 21:46:04 2012 +0100 @@ -306,7 +306,7 @@ (*Renaming of parameters in a subgoal*) fun rename_tac xs i = - case Library.find_first (not o Lexicon.is_identifier) xs of + case Library.find_first (not o Symbol_Pos.is_identifier) xs of SOME x => error ("Not an identifier: " ^ x) | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i)); diff -r 98d35a7368bd -r fb579401dc26 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/ZF/Tools/datatype_package.ML Mon Nov 26 21:46:04 2012 +0100 @@ -130,7 +130,7 @@ (*The function variable for a single constructor*) fun add_case ((_, T, _), name, args, _) (opno, cases) = - if Lexicon.is_identifier name then + if Symbol_Pos.is_identifier name then (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases) else (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) diff -r 98d35a7368bd -r fb579401dc26 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Mon Nov 26 21:10:42 2012 +0100 +++ b/src/ZF/Tools/inductive_package.ML Mon Nov 26 21:46:04 2012 +0100 @@ -78,7 +78,7 @@ and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); val rec_base_names = map Long_Name.base_name rec_names; - val dummy = assert_all Lexicon.is_identifier rec_base_names + val dummy = assert_all Symbol_Pos.is_identifier rec_base_names (fn a => "Base name of recursive set not an identifier: " ^ a); local (*Checking the introduction rules*)