# HG changeset patch # User wenzelm # Date 1302273254 -7200 # Node ID b1f544c84040629b29df105789526b0a61e54b4d # Parent dafae095d73337adb3a97225988784efd0e758dd discontinued special treatment of structure Lexicon; diff -r dafae095d733 -r b1f544c84040 NEWS --- 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. diff -r dafae095d733 -r b1f544c84040 doc-src/antiquote_setup.ML --- 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 (!?) *) diff -r dafae095d733 -r b1f544c84040 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- 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) diff -r dafae095d733 -r b1f544c84040 src/HOL/HOLCF/Tools/cont_consts.ML --- 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 diff -r dafae095d733 -r b1f544c84040 src/HOL/HOLCF/ex/Pattern_Match.thy --- 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 diff -r dafae095d733 -r b1f544c84040 src/HOL/Import/proof_kernel.ML --- 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")) (); diff -r dafae095d733 -r b1f544c84040 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- 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 diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/Datatype/datatype_aux.ML --- 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 _ = ""; diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/Datatype/datatype_case.ML --- 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) => diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/Datatype/datatype_data.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/Datatype/datatype_prop.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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) ^ diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/choice_specification.ML --- 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 diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/float_syntax.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/numeral_syntax.ML --- 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 diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/record.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/string_syntax.ML --- 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"}, diff -r dafae095d733 -r b1f544c84040 src/HOL/Tools/typedef.ML --- 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 *) diff -r dafae095d733 -r b1f544c84040 src/HOL/ex/Binary.thy --- 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); diff -r dafae095d733 -r b1f544c84040 src/HOL/ex/Numeral.thy --- 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 diff -r dafae095d733 -r b1f544c84040 src/Pure/Isar/expression.ML --- 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) diff -r dafae095d733 -r b1f544c84040 src/Pure/Isar/proof_context.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/Pure/Isar/token.ML --- 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 = diff -r dafae095d733 -r b1f544c84040 src/Pure/ML/ml_antiquote.ML --- 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" diff -r dafae095d733 -r b1f544c84040 src/Pure/ML/ml_syntax.ML --- 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 *) diff -r dafae095d733 -r b1f544c84040 src/Pure/Proof/proof_syntax.ML --- 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\\_./ _)", [0, 3], 3)), - (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), - (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] + (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4)), + (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\/ _)", [4, 5], 4))] |> Sign.add_modesyntax_i ("latex", false) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\_./ _)", [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"])])]); diff -r dafae095d733 -r b1f544c84040 src/Pure/Syntax/lexicon.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/Pure/Syntax/local_syntax.ML --- 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) diff -r dafae095d733 -r b1f544c84040 src/Pure/Syntax/syntax.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/Pure/Syntax/syntax_phases.ML --- 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) => diff -r dafae095d733 -r b1f544c84040 src/Pure/Thy/latex.ML --- 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 diff -r dafae095d733 -r b1f544c84040 src/Pure/Thy/thy_syntax.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/Pure/consts.ML --- 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); diff -r dafae095d733 -r b1f544c84040 src/Pure/pure_thy.ML --- 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; diff -r dafae095d733 -r b1f544c84040 src/Pure/sign.ML --- 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 diff -r dafae095d733 -r b1f544c84040 src/Pure/tactic.ML --- 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)); diff -r dafae095d733 -r b1f544c84040 src/ZF/Tools/datatype_package.ML --- 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) diff -r dafae095d733 -r b1f544c84040 src/ZF/Tools/inductive_package.ML --- 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*) diff -r dafae095d733 -r b1f544c84040 src/ZF/Tools/numeral_syntax.ML --- 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)