--- a/NEWS Fri Apr 08 15:48:14 2011 +0200
+++ b/NEWS Fri Apr 08 16:34:14 2011 +0200
@@ -93,10 +93,11 @@
be disabled via the configuration option Syntax.positions, which is
called "syntax_positions" in Isar attribute syntax.
-* Discontinued special treatment of various ML structures of inner
-syntax, such as structure Ast: no pervasive content, no inclusion in
-structure Syntax. INCOMPATIBILITY, refer to qualified names like
-Ast.Constant etc.
+* Discontinued special status of various ML structures that contribute
+to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less
+pervasive content, no inclusion in structure Syntax. INCOMPATIBILITY,
+refer directly to Ast.Constant, Lexicon.is_identifier,
+Syntax_Trans.mk_binder_tr etc.
* Typed print translation: discontinued show_sorts argument, which is
already available via context of "advanced" translation.
--- a/doc-src/antiquote_setup.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/doc-src/antiquote_setup.ML Fri Apr 08 16:34:14 2011 +0200
@@ -71,7 +71,8 @@
if txt2 = "" then txt1
else if kind = "type" then txt1 ^ " = " ^ txt2
else if kind = "exception" then txt1 ^ " of " ^ txt2
- else if Syntax.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2
+ else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1))
+ then txt1 ^ ": " ^ txt2
else txt1 ^ " : " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *)
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Fri Apr 08 16:34:14 2011 +0200
@@ -442,7 +442,7 @@
(* define syntax for case combinator *)
(* TODO: re-implement case syntax using a parse translation *)
local
- fun syntax c = Syntax.mark_const (fst (dest_Const c))
+ fun syntax c = Lexicon.mark_const (fst (dest_Const c))
fun xconst c = Long_Name.base_name (fst (dest_Const c))
fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
fun showint n = string_of_int (n+1)
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Fri Apr 08 16:34:14 2011 +0200
@@ -47,7 +47,7 @@
*)
fun transform thy (c, T, mx) =
let
- fun syntax b = Syntax.mark_const (Sign.full_bname thy b)
+ fun syntax b = Lexicon.mark_const (Sign.full_bname thy b)
val c1 = Binding.name_of c
val c2 = c1 ^ "_cont_syntax"
val n = Mixfix.mixfix_args mx
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Fri Apr 08 16:34:14 2011 +0200
@@ -497,7 +497,7 @@
(* syntax translations for pattern combinators *)
local
- fun syntax c = Syntax.mark_const (fst (dest_Const c));
+ fun syntax c = Lexicon.mark_const (fst (dest_Const c));
fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
val capp = app @{const_syntax Rep_cfun};
val capps = Library.foldl capp
--- a/src/HOL/Import/proof_kernel.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Import/proof_kernel.ML Fri Apr 08 16:34:14 2011 +0200
@@ -181,11 +181,11 @@
val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix;
fun mk_syn thy c =
- if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
+ if Lexicon.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
else Delimfix (Syntax_Ext.escape c)
fun quotename c =
- if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
+ if Lexicon.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
fun simple_smart_string_of_cterm ctxt0 ct =
let
@@ -454,7 +454,7 @@
val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table)
val invented_isavar = Unsynchronized.ref 0
-fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
+fun innocent_varname s = Lexicon.is_identifier s andalso not (String.isPrefix "u_" s)
fun valid_boundvarname s =
can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) ();
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 08 16:34:14 2011 +0200
@@ -32,7 +32,7 @@
let
fun cart t u = Syntax.const @{type_syntax cart} $ t $ u;
fun finite_cart_tr [t, u as Free (x, _)] =
- if Syntax.is_tid x then
+ if Lexicon.is_tid x then
cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
else cart t u
| finite_cart_tr [t, u] = cart t u
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Apr 08 16:34:14 2011 +0200
@@ -232,7 +232,7 @@
fun name_of_typ (Type (s, Ts)) =
let val s' = Long_Name.base_name s
in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
- [if Syntax.is_identifier s' then s' else "x"])
+ [if Lexicon.is_identifier s' then s' else "x"])
end
| name_of_typ _ = "";
--- a/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Fri Apr 08 16:34:14 2011 +0200
@@ -418,7 +418,7 @@
| _ => NONE);
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
-val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT);
+val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
(* destruct nested patterns *)
@@ -455,7 +455,7 @@
Syntax.const @{syntax_const "_case1"} $
map_aterms
(fn Free p => Syntax_Trans.mark_boundT p
- | Const (s, _) => Syntax.const (Syntax.mark_const s)
+ | Const (s, _) => Syntax.const (Lexicon.mark_const s)
| t => t) pat $
map_aterms
(fn x as Free (s, T) =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 16:34:14 2011 +0200
@@ -224,7 +224,7 @@
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
- let val case_name' = Syntax.mark_const case_name
+ let val case_name' = Lexicon.mark_const case_name
in (case_name', Datatype_Case.case_tr' info_of_case case_name')
end) case_names, []) thy;
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Fri Apr 08 16:34:14 2011 +0200
@@ -49,7 +49,7 @@
fun type_name (TFree (name, _)) = unprefix "'" name
| type_name (Type (name, _)) =
let val name' = Long_Name.base_name name
- in if Syntax.is_identifier name' then name' else "x" end;
+ in if Lexicon.is_identifier name' then name' else "x" end;
in indexify_names (map type_name Ts) end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Fri Apr 08 16:34:14 2011 +0200
@@ -99,7 +99,7 @@
fun needs_quoting reserved s =
Symtab.defined reserved s orelse
- exists (not o Syntax.is_identifier) (Long_Name.explode s)
+ exists (not o Lexicon.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_util.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 08 16:34:14 2011 +0200
@@ -72,7 +72,7 @@
val unyxml = XML.content_of o YXML.parse_body
-val is_long_identifier = forall Syntax.is_identifier o space_explode "."
+val is_long_identifier = forall Lexicon.is_identifier o space_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/choice_specification.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/choice_specification.ML Fri Apr 08 16:34:14 2011 +0200
@@ -160,7 +160,7 @@
let
val T = type_of c
val cname = Long_Name.base_name (fst (dest_Const c))
- val vname = if Syntax.is_identifier cname
+ val vname = if Lexicon.is_identifier cname
then cname
else "x"
in
--- a/src/HOL/Tools/float_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/float_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -27,7 +27,7 @@
fun mk_frac str =
let
- val {mant = i, exp = n} = Syntax.read_float str;
+ val {mant = i, exp = n} = Lexicon.read_float str;
val exp = Syntax.const @{const_syntax Power.power};
val ten = mk_number 10;
val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
--- a/src/HOL/Tools/numeral_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -22,7 +22,7 @@
fun mk 0 = Syntax.const @{const_name Int.Pls}
| mk ~1 = Syntax.const @{const_name Int.Min}
| mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
- in mk (#value (Syntax.read_xnum num)) end;
+ in mk (#value (Lexicon.read_xnum num)) end;
in
--- a/src/HOL/Tools/record.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/record.ML Fri Apr 08 16:34:14 2011 +0200
@@ -715,7 +715,7 @@
val more' = mk_ext rest;
in
list_comb
- (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
+ (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
@@ -760,7 +760,7 @@
let
val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
val more' = mk_ext rest;
- in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
+ in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
| mk_ext [] = more;
@@ -889,14 +889,14 @@
fun record_ext_type_tr' name =
let
- val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
+ val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
in (ext_type_name, tr') end;
fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
let
- val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
+ val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
fun tr' ctxt ts =
record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
(list_comb (Syntax.const ext_type_name, ts));
@@ -919,7 +919,7 @@
fun strip_fields t =
(case strip_comb t of
(Const (ext, _), args as (_ :: _)) =>
- (case try (Syntax.unmark_const o unsuffix extN) ext of
+ (case try (Lexicon.unmark_const o unsuffix extN) ext of
SOME ext' =>
(case get_extfields thy ext' of
SOME fields =>
@@ -946,7 +946,7 @@
fun record_ext_tr' name =
let
- val ext_name = Syntax.mark_const (name ^ extN);
+ val ext_name = Lexicon.mark_const (name ^ extN);
fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
in (ext_name, tr') end;
@@ -956,7 +956,7 @@
local
fun dest_update ctxt c =
- (case try Syntax.unmark_const c of
+ (case try Lexicon.unmark_const c of
SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
| NONE => NONE);
@@ -982,7 +982,7 @@
fun field_update_tr' name =
let
- val update_name = Syntax.mark_const (name ^ updateN);
+ val update_name = Lexicon.mark_const (name ^ updateN);
fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
| tr' _ _ = raise Match;
in (update_name, tr') end;
--- a/src/HOL/Tools/string_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/string_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -16,11 +16,11 @@
(* nibble *)
val mk_nib =
- Ast.Constant o Syntax.mark_const o
+ Ast.Constant o Lexicon.mark_const o
fst o Term.dest_Const o HOLogic.mk_nibble;
fun dest_nib (Ast.Constant s) =
- (case try Syntax.unmark_const s of
+ (case try Lexicon.unmark_const s of
NONE => raise Match
| SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
@@ -44,11 +44,12 @@
| dest_char _ = raise Match;
fun syntax_string cs =
- Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)];
+ Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
+ Ast.Variable (Lexicon.implode_xstr cs)];
fun char_ast_tr [Ast.Variable xstr] =
- (case Syntax.explode_xstr xstr of
+ (case Lexicon.explode_xstr xstr of
[c] => mk_char c
| _ => error ("Single character expected: " ^ xstr))
| char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
@@ -65,7 +66,7 @@
Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
fun string_ast_tr [Ast.Variable xstr] =
- (case Syntax.explode_xstr xstr of
+ (case Lexicon.explode_xstr xstr of
[] =>
Ast.Appl
[Ast.Constant @{syntax_const "_constrain"},
--- a/src/HOL/Tools/typedef.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/Tools/typedef.ML Fri Apr 08 16:34:14 2011 +0200
@@ -144,7 +144,7 @@
error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
val goal = mk_inhabited set;
- val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
+ val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT));
(* lhs *)
--- a/src/HOL/ex/Binary.thy Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/ex/Binary.thy Fri Apr 08 16:34:14 2011 +0200
@@ -191,11 +191,11 @@
parse_translation {*
let
val syntax_consts =
- map_aterms (fn Const (c, T) => Const (Syntax.mark_const c, T) | a => a);
+ map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
fun binary_tr [Const (num, _)] =
let
- val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
+ val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
in syntax_consts (mk_binary n) end
| binary_tr ts = raise TERM ("binary_tr", ts);
--- a/src/HOL/ex/Numeral.thy Fri Apr 08 15:48:14 2011 +0200
+++ b/src/HOL/ex/Numeral.thy Fri Apr 08 16:34:14 2011 +0200
@@ -285,7 +285,7 @@
else raise Match;
fun numeral_tr [Free (num, _)] =
let
- val {leading_zeros, value, ...} = Syntax.read_xnum num;
+ val {leading_zeros, value, ...} = Lexicon.read_xnum num;
val _ = leading_zeros = 0 andalso value > 0
orelse error ("Bad numeral: " ^ num);
in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
--- a/src/Pure/Isar/expression.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Isar/expression.ML Fri Apr 08 16:34:14 2011 +0200
@@ -613,7 +613,7 @@
(* achieve plain syntax for locale predicates (without "PROP") *)
-fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args =>
+fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
if length args = n then
Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *)
Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
--- a/src/Pure/Isar/proof_context.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Apr 08 16:34:14 2011 +0200
@@ -447,7 +447,7 @@
val tsig = tsig_of ctxt;
val (c, pos) = token_content text;
in
- if Syntax.is_tid c then
+ if Lexicon.is_tid c then
(Context_Position.report ctxt pos Markup.tfree;
TFree (c, default_sort ctxt (c, ~1)))
else
@@ -924,7 +924,7 @@
fold_map (fn (b, raw_T, mx) => fn ctxt =>
let
val x = Name.of_binding b;
- val _ = Syntax.is_identifier (no_skolem internal x) orelse
+ val _ = Lexicon.is_identifier (no_skolem internal x) orelse
error ("Illegal variable name: " ^ quote (Binding.str_of b));
fun cond_tvars T =
@@ -949,7 +949,7 @@
fun const_ast_tr intern ctxt [Ast.Variable c] =
let
val Const (c', _) = read_const_proper ctxt false c;
- val d = if intern then Syntax.mark_const c' else c;
+ val d = if intern then Lexicon.mark_const c' else c;
in Ast.Constant d end
| const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
@@ -978,13 +978,13 @@
local
fun type_syntax (Type (c, args), mx) =
- SOME (Local_Syntax.Type, (Syntax.mark_type c, Mixfix.make_type (length args), mx))
+ SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx))
| type_syntax _ = NONE;
fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
| const_syntax ctxt (Const (c, _), mx) =
(case try (Consts.type_scheme (consts_of ctxt)) c of
- SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx))
+ SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx))
| NONE => NONE)
| const_syntax _ _ = NONE;
--- a/src/Pure/Isar/token.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Isar/token.ML Fri Apr 08 16:34:14 2011 +0200
@@ -279,7 +279,7 @@
fun ident_or_symbolic "begin" = false
| ident_or_symbolic ":" = true
| ident_or_symbolic "::" = true
- | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
+ | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
(* scan verbatim text *)
@@ -335,13 +335,13 @@
(Scan.max token_leq
(Scan.literal lex2 >> pair Command)
(Scan.literal lex1 >> pair Keyword))
- (Syntax.scan_longid >> pair LongIdent ||
- Syntax.scan_id >> pair Ident ||
- Syntax.scan_var >> pair Var ||
- Syntax.scan_tid >> pair TypeIdent ||
- Syntax.scan_tvar >> pair TypeVar ||
- Syntax.scan_float >> pair Float ||
- Syntax.scan_nat >> pair Nat ||
+ (Lexicon.scan_longid >> pair LongIdent ||
+ Lexicon.scan_id >> pair Ident ||
+ Lexicon.scan_var >> pair Var ||
+ Lexicon.scan_tid >> pair TypeIdent ||
+ Lexicon.scan_tvar >> pair TypeVar ||
+ Lexicon.scan_float >> pair Float ||
+ Lexicon.scan_nat >> pair Nat ||
scan_symid >> pair SymIdent) >> uncurry token));
fun recover msg =
--- a/src/Pure/ML/ml_antiquote.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Fri Apr 08 16:34:14 2011 +0200
@@ -105,7 +105,7 @@
fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
ProofContext.read_class ctxt s
- |> syn ? Syntax.mark_class
+ |> syn ? Lexicon.mark_class
|> ML_Syntax.print_string);
val _ = inline "class" (class false);
@@ -131,7 +131,7 @@
val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
-val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
+val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c));
(* constants *)
@@ -146,7 +146,7 @@
val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
-val _ = inline "const_syntax" (const_name (fn (_, c) => Syntax.mark_const c));
+val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c));
val _ = inline "syntax_const"
--- a/src/Pure/ML/ml_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/ML/ml_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -34,7 +34,7 @@
(* reserved words *)
-val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
+val reserved_names = filter Lexicon.is_ascii_identifier ML_Lex.keywords;
val reserved = Name.make_context reserved_names;
val is_reserved = Name.is_declared reserved;
@@ -42,7 +42,7 @@
(* identifiers *)
fun is_identifier name =
- not (is_reserved name) andalso Syntax.is_ascii_identifier name;
+ not (is_reserved name) andalso Lexicon.is_ascii_identifier name;
(* literal output -- unformatted *)
--- a/src/Pure/Proof/proof_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -66,8 +66,8 @@
("", paramT --> paramsT, Delimfix "_")]
|> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
- (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
- (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
|> Sign.add_modesyntax_i ("latex", false)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
@@ -80,10 +80,10 @@
(Ast.mk_appl (Ast.Constant "_Lam")
[Ast.mk_appl (Ast.Constant "_Lam1")
[Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
- Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A",
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
(Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
- Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst"))
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
[(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
--- a/src/Pure/Syntax/lexicon.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML Fri Apr 08 16:34:14 2011 +0200
@@ -4,10 +4,11 @@
Lexer for the inner Isabelle syntax (terms and types).
*)
-signature LEXICON0 =
+signature LEXICON =
sig
val is_identifier: string -> bool
val is_ascii_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
@@ -19,37 +20,6 @@
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 implode_xstr: string list -> string
- val explode_xstr: string -> string list
- val read_indexname: string -> indexname
- val read_var: string -> term
- val read_variable: string -> indexname option
- val const: string -> term
- val free: string -> term
- val var: indexname -> term
- val read_nat: string -> int option
- val read_int: string -> int option
- val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
- val read_float: string -> {mant: int, exp: int}
- val mark_class: string -> string val unmark_class: string -> string
- val mark_type: string -> string val unmark_type: string -> string
- val mark_const: string -> string val unmark_const: string -> string
- val mark_fixed: string -> string val unmark_fixed: string -> string
- val unmark:
- {case_class: string -> 'a,
- case_type: string -> 'a,
- case_const: string -> 'a,
- case_fixed: string -> 'a,
- case_default: string -> 'a} -> string -> 'a
- val is_marked: string -> bool
- val dummy_type: term
- val fun_type: term
-end;
-
-signature LEXICON =
-sig
- include LEXICON0
- val is_xid: string -> bool
datatype token_kind =
Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
@@ -73,7 +43,32 @@
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
+ val implode_xstr: string list -> string
+ val explode_xstr: string -> string list
val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
+ val read_indexname: string -> indexname
+ val const: string -> term
+ val free: string -> term
+ val var: indexname -> term
+ val read_var: string -> term
+ val read_variable: string -> indexname option
+ val read_nat: string -> int option
+ val read_int: string -> int option
+ val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
+ val read_float: string -> {mant: int, exp: int}
+ val mark_class: string -> string val unmark_class: string -> string
+ val mark_type: string -> string val unmark_type: string -> string
+ val mark_const: string -> string val unmark_const: string -> string
+ val mark_fixed: string -> string val unmark_fixed: string -> string
+ val unmark:
+ {case_class: string -> 'a,
+ case_type: string -> 'a,
+ case_const: string -> 'a,
+ case_fixed: string -> 'a,
+ case_default: string -> 'a} -> string -> 'a
+ val is_marked: string -> bool
+ val dummy_type: term
+ val fun_type: term
end;
structure Lexicon: LEXICON =
@@ -352,37 +347,6 @@
in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
-(* logical entities *)
-
-fun marker s = (prefix s, unprefix s);
-
-val (mark_class, unmark_class) = marker "\\<^class>";
-val (mark_type, unmark_type) = marker "\\<^type>";
-val (mark_const, unmark_const) = marker "\\<^const>";
-val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
-
-fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
- (case try unmark_class s of
- SOME c => case_class c
- | NONE =>
- (case try unmark_type s of
- SOME c => case_type c
- | NONE =>
- (case try unmark_const s of
- SOME c => case_const c
- | NONE =>
- (case try unmark_fixed s of
- SOME c => case_fixed c
- | NONE => case_default s))));
-
-val is_marked =
- unmark {case_class = K true, case_type = K true, case_const = K true,
- case_fixed = K true, case_default = K false};
-
-val dummy_type = const (mark_type "dummy");
-val fun_type = const (mark_type "fun");
-
-
(* read numbers *)
local
@@ -456,4 +420,35 @@
exp = length fracpart}
end;
+
+(* marked logical entities *)
+
+fun marker s = (prefix s, unprefix s);
+
+val (mark_class, unmark_class) = marker "\\<^class>";
+val (mark_type, unmark_type) = marker "\\<^type>";
+val (mark_const, unmark_const) = marker "\\<^const>";
+val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
+
+fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
+ (case try unmark_class s of
+ SOME c => case_class c
+ | NONE =>
+ (case try unmark_type s of
+ SOME c => case_type c
+ | NONE =>
+ (case try unmark_const s of
+ SOME c => case_const c
+ | NONE =>
+ (case try unmark_fixed s of
+ SOME c => case_fixed c
+ | NONE => case_default s))));
+
+val is_marked =
+ unmark {case_class = K true, case_type = K true, case_const = K true,
+ case_fixed = K true, case_default = K false};
+
+val dummy_type = const (mark_type "dummy");
+val fun_type = const (mark_type "fun");
+
end;
--- a/src/Pure/Syntax/local_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Syntax/local_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -83,7 +83,7 @@
| prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
| prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
| prep_mixfix add mode (Fixed, (x, T, mx)) =
- SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
+ SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
fun prep_struct (Fixed, (c, _, Structure)) = SOME c
| prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
--- a/src/Pure/Syntax/syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -7,8 +7,10 @@
signature SYNTAX =
sig
- include LEXICON0
val max_pri: int
+ val const: string -> term
+ val free: string -> term
+ val var: indexname -> term
val root: string Config.T
val positions_raw: Config.raw
val positions: bool Config.T
@@ -143,6 +145,11 @@
val max_pri = Syntax_Ext.max_pri;
+val const = Lexicon.const;
+val free = Lexicon.free;
+val var = Lexicon.var;
+
+
(** inner syntax operations **)
@@ -719,11 +726,5 @@
val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
-
-(*export parts of internal Syntax structures*)
-val syntax_tokenize = tokenize;
-open Lexicon;
-val tokenize = syntax_tokenize;
-
end;
--- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 16:34:14 2011 +0200
@@ -434,9 +434,9 @@
fun term_of (Type (a, Ts)) =
Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
| term_of (TFree (x, S)) =
- if is_some (Term_Position.decode x) then Lexicon.free x
- else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
- | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
+ if is_some (Term_Position.decode x) then Syntax.free x
+ else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S
+ | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S;
in term_of ty end;
@@ -514,11 +514,11 @@
fun prune_typs (t_seen as (Const _, _)) = t_seen
| prune_typs (t as Free (x, ty), seen) =
if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
else (t, t :: seen)
| prune_typs (t as Var (xi, ty), seen) =
if ty = dummyT then (t, seen)
- else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
+ else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
else (t, t :: seen)
| prune_typs (t_seen as (Bound _, _)) = t_seen
| prune_typs (Abs (x, ty, t), seen) =
@@ -534,11 +534,11 @@
(case strip_comb tm of
(t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
| ((c as Const ("_free", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+ Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
| ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
+ Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
| ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
- Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+ Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
| (Const ("_idtdummy", T), ts) =>
Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
| (const as Const (c, T), ts) =>
--- a/src/Pure/Thy/latex.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Thy/latex.ML Fri Apr 08 16:34:14 2011 +0200
@@ -130,7 +130,7 @@
if invisible_token tok then ""
else if Token.is_kind Token.Command tok then
"\\isacommand{" ^ output_syms s ^ "}"
- else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
+ else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
"\\isakeyword{" ^ output_syms s ^ "}"
else if Token.is_kind Token.String tok then
output_syms s |> enclose
--- a/src/Pure/Thy/thy_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -65,7 +65,7 @@
| Token.EOF => Markup.control;
fun token_markup tok =
- if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator
+ if Token.keyword_with (not o Lexicon.is_identifier) tok then Markup.operator
else
let
val kind = Token.kind_of tok;
--- a/src/Pure/consts.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/consts.ML Fri Apr 08 16:34:14 2011 +0200
@@ -132,12 +132,12 @@
val extern = Name_Space.extern o space_of;
fun intern_syntax consts s =
- (case try Syntax.unmark_const s of
+ (case try Lexicon.unmark_const s of
SOME c => c
| NONE => intern consts s);
fun extern_syntax consts s =
- (case try Syntax.unmark_const s of
+ (case try Lexicon.unmark_const s of
SOME c => extern consts c
| NONE => s);
--- a/src/Pure/pure_thy.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 08 16:34:14 2011 +0200
@@ -16,8 +16,8 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
-val tycon = Syntax.mark_type;
-val const = Syntax.mark_const;
+val tycon = Lexicon.mark_type;
+val const = Lexicon.mark_const;
val typeT = Syntax_Ext.typeT;
val spropT = Syntax_Ext.spropT;
--- a/src/Pure/sign.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/sign.ML Fri Apr 08 16:34:14 2011 +0200
@@ -334,7 +334,7 @@
fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
let
fun type_syntax (b, n, mx) =
- (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
+ (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
in (naming, syn', tsig', consts) end);
@@ -373,7 +373,7 @@
fun type_notation add mode args =
let
fun type_syntax (Type (c, args), mx) =
- SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
+ SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
| type_syntax _ = NONE;
in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
@@ -381,7 +381,7 @@
let
fun const_syntax (Const (c, _), mx) =
(case try (Consts.type_scheme (consts_of thy)) c of
- SOME T => SOME (Syntax.mark_const c, T, mx)
+ SOME T => SOME (Lexicon.mark_const c, T, mx)
| NONE => NONE)
| const_syntax _ = NONE;
in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
@@ -401,7 +401,7 @@
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
val T' = Logic.varifyT_global T;
- in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
+ in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
val args = map prep raw_args;
in
thy
--- a/src/Pure/tactic.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/Pure/tactic.ML Fri Apr 08 16:34:14 2011 +0200
@@ -318,7 +318,7 @@
(*Renaming of parameters in a subgoal*)
fun rename_tac xs i =
- case Library.find_first (not o Syntax.is_identifier) xs of
+ case Library.find_first (not o Lexicon.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 Fri Apr 08 15:48:14 2011 +0200
+++ b/src/ZF/Tools/datatype_package.ML Fri Apr 08 16:34:14 2011 +0200
@@ -130,7 +130,7 @@
(*The function variable for a single constructor*)
fun add_case ((_, T, _), name, args, _) (opno, cases) =
- if Syntax.is_identifier name then
+ if Lexicon.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 Fri Apr 08 15:48:14 2011 +0200
+++ b/src/ZF/Tools/inductive_package.ML Fri Apr 08 16:34:14 2011 +0200
@@ -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 Syntax.is_identifier rec_base_names
+ val dummy = assert_all Lexicon.is_identifier rec_base_names
(fn a => "Base name of recursive set not an identifier: " ^ a);
local (*Checking the introduction rules*)
--- a/src/ZF/Tools/numeral_syntax.ML Fri Apr 08 15:48:14 2011 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML Fri Apr 08 16:34:14 2011 +0200
@@ -71,7 +71,7 @@
(* translation of integer constant tokens to and from binary *)
fun int_tr [t as Free (str, _)] =
- Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
+ Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str))
| int_tr ts = raise TERM ("int_tr", ts);
fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)