--- a/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML Sun Feb 21 22:35:02 2010 +0100
@@ -422,8 +422,7 @@
| _ => NONE;
val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
-val dest_case' = gen_dest_case
- (try (dest_Const #> fst #> unprefix Syntax.constN)) (K dummyT);
+val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT);
(* destruct nested patterns *)
@@ -461,7 +460,7 @@
Syntax.const @{syntax_const "_case1"} $
map_aterms
(fn Free p => Syntax.mark_boundT p
- | Const (s, _) => Syntax.const (Syntax.constN ^ s)
+ | Const (s, _) => Syntax.const (Syntax.mark_const s)
| t => t) pat $
map_aterms
(fn x as Free (s, T) =>
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Feb 21 22:35:02 2010 +0100
@@ -223,7 +223,7 @@
fun add_case_tr' case_names thy =
Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
- let val case_name' = Syntax.constN ^ case_name
+ let val case_name' = Syntax.mark_const case_name
in (case_name', Datatype_Case.case_tr' info_of_case case_name')
end) case_names, []) thy;
--- a/src/HOL/Tools/record.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOL/Tools/record.ML Sun Feb 21 22:35:02 2010 +0100
@@ -799,7 +799,7 @@
let
val (args, rest) = split_args (map fst (but_last fields)) fargs;
val more' = mk_ext rest;
- in list_comb (Syntax.const (Syntax.constN ^ ext ^ extN), args @ [more']) end
+ in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
| NONE => err ("no fields defined for " ^ ext))
| NONE => err (name ^ " is no proper field"))
| mk_ext [] = more;
@@ -977,7 +977,7 @@
fun strip_fields t =
(case strip_comb t of
(Const (ext, _), args as (_ :: _)) =>
- (case try (unprefix Syntax.constN o unsuffix extN) ext of
+ (case try (Syntax.unmark_const o unsuffix extN) ext of
SOME ext' =>
(case get_extfields thy ext' of
SOME fields =>
@@ -1004,7 +1004,7 @@
fun record_ext_tr' name =
let
- val ext_name = Syntax.constN ^ name ^ extN;
+ val ext_name = Syntax.mark_const (name ^ extN);
fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
in (ext_name, tr') end;
@@ -1024,7 +1024,7 @@
if null (loose_bnos t) then t else raise Match
| _ => raise Match);
in
- (case try (unprefix Syntax.constN) c |> Option.map extern of
+ (case Option.map extern (try Syntax.unmark_const c) of
SOME update_name =>
(case try (unsuffix updateN) update_name of
SOME name =>
@@ -1046,7 +1046,7 @@
fun field_update_tr' name =
let
- val update_name = Syntax.constN ^ name ^ updateN;
+ val update_name = Syntax.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 Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOL/Tools/string_syntax.ML Sun Feb 21 22:35:02 2010 +0100
@@ -16,11 +16,11 @@
(* nibble *)
val mk_nib =
- Syntax.Constant o prefix Syntax.constN o
+ Syntax.Constant o Syntax.mark_const o
fst o Term.dest_Const o HOLogic.mk_nibble;
fun dest_nib (Syntax.Constant s) =
- (case try (unprefix Syntax.constN) s of
+ (case try Syntax.unmark_const s of
NONE => raise Match
| SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
--- a/src/HOL/ex/Binary.thy Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOL/ex/Binary.thy Sun Feb 21 22:35:02 2010 +0100
@@ -191,7 +191,7 @@
parse_translation {*
let
val syntax_consts =
- map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
+ map_aterms (fn Const (c, T) => Const (Syntax.mark_const c, T) | a => a);
fun binary_tr [Const (num, _)] =
let
--- a/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Sun Feb 21 22:35:02 2010 +0100
@@ -114,7 +114,7 @@
(* ----- case translation --------------------------------------------------- *)
- fun syntax b = Syntax.constN ^ Sign.full_bname thy b;
+ fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
local open Syntax in
local
--- a/src/HOLCF/Tools/cont_consts.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML Sun Feb 21 22:35:02 2010 +0100
@@ -46,7 +46,7 @@
*)
fun transform thy (c, T, mx) =
let
- fun syntax b = Syntax.constN ^ Sign.full_bname thy b;
+ fun syntax b = Syntax.mark_const (Sign.full_bname thy b);
val c1 = Binding.name_of c;
val c2 = c1 ^ "_cont_syntax";
val n = Syntax.mixfix_args mx;
--- a/src/Pure/Isar/expression.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/Isar/expression.ML Sun Feb 21 22:35:02 2010 +0100
@@ -604,7 +604,7 @@
(* achieve plain syntax for locale predicates (without "PROP") *)
-fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args =>
+fun aprop_tr' n c = (Syntax.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 Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Feb 21 22:35:02 2010 +0100
@@ -988,7 +988,7 @@
fun const_ast_tr intern ctxt [Syntax.Variable c] =
let
val Const (c', _) = read_const_proper ctxt c;
- val d = if intern then Syntax.constN ^ c' else c;
+ val d = if intern then Syntax.mark_const c' else c;
in Syntax.Constant d end
| const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
@@ -1017,7 +1017,7 @@
fun const_syntax _ (Free (x, T), mx) = SOME (true, (x, T, mx))
| const_syntax ctxt (Const (c, _), mx) =
(case try (Consts.type_scheme (consts_of ctxt)) c of
- SOME T => SOME (false, (Syntax.constN ^ c, T, mx))
+ SOME T => SOME (false, (Syntax.mark_const c, T, mx))
| NONE => NONE)
| const_syntax _ _ = NONE;
--- a/src/Pure/ML/ml_antiquote.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Sun Feb 21 22:35:02 2010 +0100
@@ -114,7 +114,7 @@
fun const syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
#1 (Term.dest_Const (ProofContext.read_const_proper ctxt c))
- |> syn ? prefix Syntax.constN
+ |> syn ? Syntax.mark_const
|> ML_Syntax.print_string);
val _ = inline "const_name" (const false);
--- a/src/Pure/Proof/proof_syntax.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Sun Feb 21 22:35:02 2010 +0100
@@ -67,8 +67,8 @@
("", paramT --> paramsT, Delimfix "_")]
|> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
- (Syntax.constN ^ "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
- (Syntax.constN ^ "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
+ (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))]
|> Sign.add_modesyntax_i ("latex", false)
[("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
|> Sign.add_trrules_i (map Syntax.ParsePrintRule
@@ -78,10 +78,10 @@
[Variable "l", Syntax.mk_appl (Constant "_Lam") [Variable "m", Variable "A"]]),
(Syntax.mk_appl (Constant "_Lam")
[Syntax.mk_appl (Constant "_Lam1") [Variable "x", Variable "A"], Variable "B"],
- Syntax.mk_appl (Constant (Syntax.constN ^ "AbsP")) [Variable "A",
+ Syntax.mk_appl (Constant (Syntax.mark_const "AbsP")) [Variable "A",
(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "B"])]),
(Syntax.mk_appl (Constant "_Lam") [Variable "x", Variable "A"],
- Syntax.mk_appl (Constant (Syntax.constN ^ "Abst"))
+ Syntax.mk_appl (Constant (Syntax.mark_const "Abst"))
[(Syntax.mk_appl (Constant "_abs") [Variable "x", Variable "A"])])]);
--- a/src/Pure/Syntax/lexicon.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/Syntax/lexicon.ML Sun Feb 21 22:35:02 2010 +0100
@@ -31,7 +31,11 @@
val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
val read_float: string -> {mant: int, exp: int}
val fixedN: string
+ val mark_fixed: string -> string
+ val unmark_fixed: string -> string
val constN: string
+ val mark_const: string -> string
+ val unmark_const: string -> string
end;
signature LEXICON =
@@ -331,8 +335,13 @@
(* specific identifiers *)
+val fixedN = "\\<^fixed>";
+val mark_fixed = prefix fixedN;
+val unmark_fixed = unprefix fixedN;
+
val constN = "\\<^const>";
-val fixedN = "\\<^fixed>";
+val mark_const = prefix constN;
+val unmark_const = unprefix constN;
(* read numbers *)
--- a/src/Pure/Syntax/printer.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/Syntax/printer.ML Sun Feb 21 22:35:02 2010 +0100
@@ -321,10 +321,10 @@
else pr, args))
and atomT a =
- (case try (unprefix Lexicon.constN) a of
+ (case try Lexicon.unmark_const a of
SOME c => Pretty.mark (Markup.const c) (Pretty.str (extern_const c))
| NONE =>
- (case try (unprefix Lexicon.fixedN) a of
+ (case try Lexicon.unmark_fixed a of
SOME x => the (token_trans "_free" x)
| NONE => Pretty.str a))
@@ -340,8 +340,8 @@
let
val nargs = length args;
val markup = Pretty.mark
- (Markup.const (unprefix Lexicon.constN a) handle Fail _ =>
- (Markup.fixed (unprefix Lexicon.fixedN a)))
+ (Markup.const (Lexicon.unmark_const a) handle Fail _ =>
+ (Markup.fixed (Lexicon.unmark_fixed a)))
handle Fail _ => I;
(*find matching table entry, or print as prefix / postfix*)
--- a/src/Pure/Syntax/type_ext.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML Sun Feb 21 22:35:02 2010 +0100
@@ -123,7 +123,9 @@
| decode (t $ u) = decode t $ decode u
| decode (Const (a, T)) =
let val c =
- (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a))
+ (case try Lexicon.unmark_const a of
+ SOME c => c
+ | NONE => snd (map_const a))
in Const (c, map_type T) end
| decode (Free (a, T)) =
(case (map_free a, map_const a) of
--- a/src/Pure/consts.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/consts.ML Sun Feb 21 22:35:02 2010 +0100
@@ -127,7 +127,7 @@
val extern = Name_Space.extern o space_of;
fun intern_syntax consts name =
- (case try (unprefix Syntax.constN) name of
+ (case try Syntax.unmark_const name of
SOME c => c
| NONE => intern consts name);
--- a/src/Pure/pure_thy.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/pure_thy.ML Sun Feb 21 22:35:02 2010 +0100
@@ -225,7 +225,7 @@
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
-val const = prefix Syntax.constN;
+val const = Syntax.mark_const;
val typeT = Syntax.typeT;
val spropT = Syntax.spropT;
--- a/src/Pure/sign.ML Sun Feb 21 21:41:29 2010 +0100
+++ b/src/Pure/sign.ML Sun Feb 21 22:35:02 2010 +0100
@@ -297,7 +297,7 @@
val intern_typ = typ_mapping intern_class intern_type;
val extern_typ = typ_mapping extern_class extern_type;
val intern_term = term_mapping intern_class intern_type intern_const;
-val extern_term = term_mapping extern_class extern_type (fn _ => fn c => Syntax.constN ^ c);
+val extern_term = term_mapping extern_class extern_type (K Syntax.mark_const);
val intern_tycons = typ_mapping (K I) intern_type;
end;
@@ -486,7 +486,7 @@
val change_gram = if add then Syntax.update_const_gram else Syntax.remove_const_gram;
fun const_syntax (Const (c, _), mx) =
(case try (Consts.type_scheme (consts_of thy)) c of
- SOME T => SOME (Syntax.constN ^ c, T, mx)
+ SOME T => SOME (Syntax.mark_const c, T, mx)
| NONE => NONE)
| const_syntax _ = NONE;
in gen_syntax change_gram (K I) mode (map_filter const_syntax args) thy end;
@@ -503,11 +503,10 @@
fun prep (b, raw_T, mx) =
let
val c = full_name thy b;
- val c_syn = Syntax.constN ^ c;
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 T;
- in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
+ in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
val args = map prep raw_args;
in
thy