1.1 --- a/src/Doc/antiquote_setup.ML Mon Nov 26 21:10:42 2012 +0100
1.2 +++ b/src/Doc/antiquote_setup.ML Mon Nov 26 21:46:04 2012 +0100
1.3 @@ -80,7 +80,7 @@
1.4 if txt2 = "" then txt1
1.5 else if kind = "type" then txt1 ^ " = " ^ txt2
1.6 else if kind = "exception" then txt1 ^ " of " ^ txt2
1.7 - else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1))
1.8 + else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
1.9 then txt1 ^ ": " ^ txt2
1.10 else txt1 ^ " : " ^ txt2;
1.11 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
2.1 --- a/src/HOL/Tools/ATP/atp_util.ML Mon Nov 26 21:10:42 2012 +0100
2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Mon Nov 26 21:46:04 2012 +0100
2.3 @@ -126,7 +126,7 @@
2.4
2.5 val unyxml = XML.content_of o YXML.parse_body
2.6
2.7 -val is_long_identifier = forall Lexicon.is_identifier o Long_Name.explode
2.8 +val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
2.9 fun maybe_quote y =
2.10 let val s = unyxml y in
2.11 y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
3.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML Mon Nov 26 21:10:42 2012 +0100
3.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Nov 26 21:46:04 2012 +0100
3.3 @@ -232,7 +232,7 @@
3.4 let val s' = Long_Name.base_name s in
3.5 space_implode "_"
3.6 (filter_out (equal "") (map name_of_typ Ts) @
3.7 - [if Lexicon.is_identifier s' then s' else "x"])
3.8 + [if Symbol_Pos.is_identifier s' then s' else "x"])
3.9 end
3.10 | name_of_typ _ = "";
3.11
4.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML Mon Nov 26 21:10:42 2012 +0100
4.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Mon Nov 26 21:46:04 2012 +0100
4.3 @@ -46,7 +46,7 @@
4.4 fun type_name (TFree (name, _)) = unprefix "'" name
4.5 | type_name (Type (name, _)) =
4.6 let val name' = Long_Name.base_name name
4.7 - in if Lexicon.is_identifier name' then name' else "x" end;
4.8 + in if Symbol_Pos.is_identifier name' then name' else "x" end;
4.9 in indexify_names (map type_name Ts) end;
4.10
4.11
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Nov 26 21:10:42 2012 +0100
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Nov 26 21:46:04 2012 +0100
5.3 @@ -61,7 +61,7 @@
5.4
5.5 fun needs_quoting reserved s =
5.6 Symtab.defined reserved s orelse
5.7 - exists (not o Lexicon.is_identifier) (Long_Name.explode s)
5.8 + exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
5.9
5.10 fun make_name reserved multi j name =
5.11 (name |> needs_quoting reserved name ? quote) ^
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Nov 26 21:10:42 2012 +0100
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Nov 26 21:46:04 2012 +0100
6.3 @@ -224,7 +224,7 @@
6.4 "using " ^ space_implode " " (map string_for_label ls) ^ " "
6.5
6.6 fun command_call name [] =
6.7 - name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
6.8 + name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
6.9 | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
6.10
6.11 fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
7.1 --- a/src/HOL/Tools/choice_specification.ML Mon Nov 26 21:10:42 2012 +0100
7.2 +++ b/src/HOL/Tools/choice_specification.ML Mon Nov 26 21:46:04 2012 +0100
7.3 @@ -166,7 +166,7 @@
7.4 let
7.5 val T = type_of c
7.6 val cname = Long_Name.base_name (fst (dest_Const c))
7.7 - val vname = if Lexicon.is_identifier cname
7.8 + val vname = if Symbol_Pos.is_identifier cname
7.9 then cname
7.10 else "x"
7.11 in
8.1 --- a/src/Pure/General/binding.ML Mon Nov 26 21:10:42 2012 +0100
8.2 +++ b/src/Pure/General/binding.ML Mon Nov 26 21:46:04 2012 +0100
8.3 @@ -136,7 +136,7 @@
8.4 fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding);
8.5
8.6 fun check binding =
8.7 - if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
8.8 + if Symbol_Pos.is_identifier (name_of binding) then ()
8.9 else legacy_feature (bad binding);
8.10
8.11 end;
9.1 --- a/src/Pure/General/symbol.ML Mon Nov 26 21:10:42 2012 +0100
9.2 +++ b/src/Pure/General/symbol.ML Mon Nov 26 21:46:04 2012 +0100
9.3 @@ -53,7 +53,6 @@
9.4 val is_block_ctrl: symbol -> bool
9.5 val is_quasi_letter: symbol -> bool
9.6 val is_letdig: symbol -> bool
9.7 - val is_ident: symbol list -> bool
9.8 val beginning: int -> symbol list -> string
9.9 val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
9.10 val explode: string -> symbol list
9.11 @@ -512,12 +511,6 @@
9.12 |> implode;
9.13
9.14
9.15 -(* identifiers *)
9.16 -
9.17 -fun is_ident [] = false
9.18 - | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
9.19 -
9.20 -
9.21 (* bump string -- treat as base 26 or base 1 numbers *)
9.22
9.23 fun symbolic_end (_ :: "\\<^isub>" :: _) = true
10.1 --- a/src/Pure/General/symbol_pos.ML Mon Nov 26 21:10:42 2012 +0100
10.2 +++ b/src/Pure/General/symbol_pos.ML Mon Nov 26 21:46:04 2012 +0100
10.3 @@ -37,6 +37,9 @@
10.4 val range: T list -> Position.range
10.5 val implode_range: Position.T -> Position.T -> T list -> text * Position.range
10.6 val explode: text * Position.T -> T list
10.7 + val scan_ident: T list -> T list * T list
10.8 + val is_ident: T list -> bool
10.9 + val is_identifier: string -> bool
10.10 end;
10.11
10.12 structure Symbol_Pos: SYMBOL_POS =
10.13 @@ -208,6 +211,18 @@
10.14 (Symbol.explode str) ([], Position.reset_range pos);
10.15 in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
10.16
10.17 +
10.18 +(* identifiers *)
10.19 +
10.20 +val scan_ident =
10.21 + Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
10.22 +
10.23 +fun is_ident [] = false
10.24 + | is_ident (s :: ss) = Symbol.is_letter (symbol s) andalso forall (Symbol.is_letdig o symbol) ss;
10.25 +
10.26 +fun is_identifier s =
10.27 + Symbol.is_ascii_identifier s orelse is_ident (explode (s, Position.none));
10.28 +
10.29 end;
10.30
10.31 structure Basic_Symbol_Pos = (*not open by default*)
11.1 --- a/src/Pure/Isar/proof_context.ML Mon Nov 26 21:10:42 2012 +0100
11.2 +++ b/src/Pure/Isar/proof_context.ML Mon Nov 26 21:46:04 2012 +0100
11.3 @@ -974,7 +974,7 @@
11.4 fold_map (fn (b, raw_T, mx) => fn ctxt =>
11.5 let
11.6 val x = Variable.check_name b;
11.7 - val _ = Lexicon.is_identifier (no_skolem internal x) orelse
11.8 + val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
11.9 error ("Illegal variable name: " ^ Binding.print b);
11.10
11.11 fun cond_tvars T =
12.1 --- a/src/Pure/Isar/token.ML Mon Nov 26 21:10:42 2012 +0100
12.2 +++ b/src/Pure/Isar/token.ML Mon Nov 26 21:46:04 2012 +0100
12.3 @@ -311,7 +311,7 @@
12.4 fun ident_or_symbolic "begin" = false
12.5 | ident_or_symbolic ":" = true
12.6 | ident_or_symbolic "::" = true
12.7 - | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
12.8 + | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s;
12.9
12.10
12.11 (* scan verbatim text *)
13.1 --- a/src/Pure/Syntax/lexicon.ML Mon Nov 26 21:10:42 2012 +0100
13.2 +++ b/src/Pure/Syntax/lexicon.ML Mon Nov 26 21:46:04 2012 +0100
13.3 @@ -12,9 +12,6 @@
13.4 val free: string -> term
13.5 val var: indexname -> term
13.6 end
13.7 - val is_identifier: string -> bool
13.8 - val is_xid: string -> bool
13.9 - val is_tid: string -> bool
13.10 val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
13.11 val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
13.12 val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
13.13 @@ -25,6 +22,7 @@
13.14 val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
13.15 val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
13.16 val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
13.17 + val is_tid: string -> bool
13.18 datatype token_kind =
13.19 Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
13.20 NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
13.21 @@ -90,32 +88,13 @@
13.22
13.23
13.24
13.25 -(** is_identifier etc. **)
13.26 -
13.27 -val is_identifier = Symbol.is_ident o Symbol.explode;
13.28 -
13.29 -fun is_xid s =
13.30 - (case Symbol.explode s of
13.31 - "_" :: cs => Symbol.is_ident cs
13.32 - | cs => Symbol.is_ident cs);
13.33 -
13.34 -fun is_tid s =
13.35 - (case Symbol.explode s of
13.36 - "'" :: cs => Symbol.is_ident cs
13.37 - | _ => false);
13.38 -
13.39 -
13.40 -
13.41 (** basic scanners **)
13.42
13.43 open Basic_Symbol_Pos;
13.44
13.45 fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
13.46
13.47 -val scan_id =
13.48 - Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
13.49 - Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
13.50 -
13.51 +val scan_id = Symbol_Pos.scan_ident;
13.52 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
13.53 val scan_tid = $$$ "'" @@@ scan_id;
13.54
13.55 @@ -130,6 +109,11 @@
13.56 val scan_var = $$$ "?" @@@ scan_id_nat;
13.57 val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
13.58
13.59 +fun is_tid s =
13.60 + (case try (unprefix "'") s of
13.61 + SOME s' => Symbol_Pos.is_identifier s'
13.62 + | NONE => false);
13.63 +
13.64
13.65
13.66 (** datatype token **)
13.67 @@ -315,7 +299,8 @@
13.68 if Symbol.is_digit c then chop_idx cs (c :: ds)
13.69 else idxname (c :: cs) ds;
13.70
13.71 - val scan = (scan_id >> map Symbol_Pos.symbol) --
13.72 + val scan =
13.73 + (scan_id >> map Symbol_Pos.symbol) --
13.74 Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
13.75 in
13.76 scan >>
14.1 --- a/src/Pure/tactic.ML Mon Nov 26 21:10:42 2012 +0100
14.2 +++ b/src/Pure/tactic.ML Mon Nov 26 21:46:04 2012 +0100
14.3 @@ -306,7 +306,7 @@
14.4
14.5 (*Renaming of parameters in a subgoal*)
14.6 fun rename_tac xs i =
14.7 - case Library.find_first (not o Lexicon.is_identifier) xs of
14.8 + case Library.find_first (not o Symbol_Pos.is_identifier) xs of
14.9 SOME x => error ("Not an identifier: " ^ x)
14.10 | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
14.11
15.1 --- a/src/ZF/Tools/datatype_package.ML Mon Nov 26 21:10:42 2012 +0100
15.2 +++ b/src/ZF/Tools/datatype_package.ML Mon Nov 26 21:46:04 2012 +0100
15.3 @@ -130,7 +130,7 @@
15.4
15.5 (*The function variable for a single constructor*)
15.6 fun add_case ((_, T, _), name, args, _) (opno, cases) =
15.7 - if Lexicon.is_identifier name then
15.8 + if Symbol_Pos.is_identifier name then
15.9 (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
15.10 else
15.11 (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
16.1 --- a/src/ZF/Tools/inductive_package.ML Mon Nov 26 21:10:42 2012 +0100
16.2 +++ b/src/ZF/Tools/inductive_package.ML Mon Nov 26 21:46:04 2012 +0100
16.3 @@ -78,7 +78,7 @@
16.4 and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
16.5
16.6 val rec_base_names = map Long_Name.base_name rec_names;
16.7 - val dummy = assert_all Lexicon.is_identifier rec_base_names
16.8 + val dummy = assert_all Symbol_Pos.is_identifier rec_base_names
16.9 (fn a => "Base name of recursive set not an identifier: " ^ a);
16.10
16.11 local (*Checking the introduction rules*)