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