--- a/doc-src/Codegen/Thy/Setup.thy Fri Apr 08 19:04:08 2011 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Sat Apr 09 13:10:20 2011 +0200
@@ -10,15 +10,13 @@
setup {*
let
val typ = Simple_Syntax.read_typ;
- val typeT = Syntax_Ext.typeT;
- val spropT = Syntax_Ext.spropT;
in
- Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
- #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+ Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
+ [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
+ Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
+ [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
*}
--- a/src/FOL/IFOL.thy Fri Apr 08 19:04:08 2011 +0200
+++ b/src/FOL/IFOL.thy Sat Apr 09 13:10:20 2011 +0200
@@ -590,7 +590,7 @@
use "fologic.ML"
-lemma thin_refl: "!!X. [|x=x; PROP W|] ==> PROP W" .
+lemma thin_refl: "[|x=x; PROP W|] ==> PROP W" .
use "hypsubstdata.ML"
setup hypsubst_setup
--- a/src/HOL/Imperative_HOL/Overview.thy Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy Sat Apr 09 13:10:20 2011 +0200
@@ -11,15 +11,13 @@
setup {*
let
val typ = Simple_Syntax.read_typ;
- val typeT = Syntax_Ext.typeT;
- val spropT = Syntax_Ext.spropT;
in
- Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
- #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+ Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
+ [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
+ Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
+ [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
*}(*>*)
--- a/src/HOL/Library/OptionalSugar.thy Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Sat Apr 09 13:10:20 2011 +0200
@@ -51,15 +51,13 @@
setup {*
let
val typ = Simple_Syntax.read_typ;
- val typeT = Syntax_Ext.typeT;
- val spropT = Syntax_Ext.spropT;
in
- Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
- #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+ Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
+ [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
+ Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
+ [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
*}
@@ -70,10 +68,10 @@
val classesT = Type ("classes", []); (*FIXME*)
in
Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
- ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
- ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
- ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
+ ("_topsort", sortT, Mixfix ("\<top>", [], 1000)),
+ ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)),
+ ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000)),
+ ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000))
]
end
*}
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sat Apr 09 13:10:20 2011 +0200
@@ -243,8 +243,7 @@
val thy = ProofContext.theory_of ctxt;
val (vs, cos) = the_spec thy dtco;
val ty = Type (dtco, map TFree vs);
- val pretty_typ_bracket =
- Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt);
+ val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
fun pretty_constr (co, tys) =
Pretty.block (Pretty.breaks
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
--- a/src/Pure/Isar/isar_syn.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat Apr 09 13:10:20 2011 +0200
@@ -161,11 +161,11 @@
val _ =
Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
- (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
+ (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
val _ =
Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
- (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
+ (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
(* translations *)
@@ -227,25 +227,25 @@
val _ =
Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
Keyword.thy_decl
- (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+ (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd true mode args));
val _ =
Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
Keyword.thy_decl
- (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
+ (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd false mode args));
val _ =
Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
Keyword.thy_decl
- (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
+ (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd true mode args));
val _ =
Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
Keyword.thy_decl
- (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
+ (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd false mode args));
@@ -626,7 +626,7 @@
val _ =
Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
(Keyword.tag_proof Keyword.prf_decl)
- (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
+ (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
>> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
val case_spec =
--- a/src/Pure/Isar/parse.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Isar/parse.ML Sat Apr 09 13:10:20 2011 +0200
@@ -78,7 +78,7 @@
val opt_mixfix: mixfix parser
val opt_mixfix': mixfix parser
val where_: string parser
- val const: (string * string * mixfix) parser
+ val const_decl: (string * string * mixfix) parser
val const_binding: (binding * string * mixfix) parser
val params: (binding * string option) list parser
val simple_fixes: (binding * string option) list parser
@@ -91,6 +91,8 @@
val prop_group: string parser
val term: string parser
val prop: string parser
+ val type_const: string parser
+ val const: string parser
val literal_fact: string parser
val propp: (string * string list) parser
val termp: (string * string list) parser
@@ -272,7 +274,7 @@
val mfix = string --
!!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
- Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
+ Scan.optional nat 1000) >> (Mixfix o triple2);
val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
@@ -295,7 +297,7 @@
val where_ = $$$ "where";
-val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+val const_decl = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val const_binding = binding -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
val params = Scan.repeat1 binding -- Scan.option ($$$ "::" |-- !!! typ)
@@ -327,6 +329,9 @@
val term = inner_syntax term_group;
val prop = inner_syntax prop_group;
+val type_const = inner_syntax (group "type constructor" xname);
+val const = inner_syntax (group "constant" xname);
+
val literal_fact = inner_syntax (group "literal fact" alt_string);
--- a/src/Pure/Isar/proof_context.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat Apr 09 13:10:20 2011 +0200
@@ -942,37 +942,6 @@
end;
-(* authentic syntax *)
-
-local
-
-fun const_ast_tr intern ctxt [Ast.Variable c] =
- let
- val Const (c', _) = read_const_proper ctxt false 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);
-
-val typ = Simple_Syntax.read_typ;
-
-in
-
-val _ = Context.>> (Context.map_theory
- (Sign.add_syntax_i
- [("_context_const", typ "id => logic", Delimfix "CONST _"),
- ("_context_const", typ "id => aprop", Delimfix "CONST _"),
- ("_context_const", typ "longid => logic", Delimfix "CONST _"),
- ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
- ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
- ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
- ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
- ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
- Sign.add_advanced_trfuns
- ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
-
-end;
-
-
(* notation *)
local
--- a/src/Pure/ML/ml_antiquote.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Sat Apr 09 13:10:20 2011 +0200
@@ -151,7 +151,8 @@
val _ = inline "syntax_const"
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) =>
- if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
+ if is_some (Syntax.lookup_const (ProofContext.syn_of ctxt) c)
+ then ML_Syntax.print_string c
else error ("Unknown syntax const: " ^ quote c ^ Position.str_of pos)));
val _ = inline "const"
--- a/src/Pure/Syntax/mixfix.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML Sat Apr 09 13:10:20 2011 +0200
@@ -88,7 +88,8 @@
(* syn_ext_types *)
-fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
+val typeT = Type ("type", []);
+fun make_type n = replicate n typeT ---> typeT;
fun syn_ext_types type_decls =
let
@@ -96,7 +97,7 @@
fun mfix_of (_, _, NoSyn) = NONE
| mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
- | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
+ | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000))
| mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
| mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
| mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
@@ -109,8 +110,8 @@
val mfix = map mfix_of type_decls;
val _ = map2 check_args type_decls mfix;
- val xconsts = map #1 type_decls;
- in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
+ val consts = map (fn (t, _, _) => (t, "")) type_decls;
+ in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end;
(* syn_ext_consts *)
@@ -121,7 +122,7 @@
fun syn_ext_consts is_logtype const_decls =
let
fun mk_infix sy ty c p1 p2 p3 =
- [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
+ [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
@@ -130,7 +131,7 @@
fun mfix_of (_, _, NoSyn) = []
| mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
- | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
+ | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)]
| mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
| mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
| mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
@@ -142,16 +143,16 @@
| binder _ = NONE;
val mfix = maps mfix_of const_decls;
- val xconsts = map #1 const_decls;
val binders = map_filter binder const_decls;
val binder_trs = binders
|> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
val binder_trs' = binders
|> map (Syntax_Ext.stamp_trfun binder_stamp o
apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
+
+ val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
in
- Syntax_Ext.syn_ext' true is_logtype
- mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
+ Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
end;
end;
--- a/src/Pure/Syntax/printer.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Syntax/printer.ML Sat Apr 09 13:10:20 2011 +0200
@@ -98,7 +98,7 @@
let
fun arg (s, p) =
(if s = "type" then TypArg else Arg)
- (if Lexicon.is_terminal s then Syntax_Ext.max_pri else p);
+ (if Lexicon.is_terminal s then 1000 else p);
fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
apfst (cons (String s)) (xsyms_to_syms xsyms)
@@ -210,10 +210,8 @@
val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
in (T :: Ts, args') end
- and parT m (pr, args, p, p': int) =
- #1 (synT m
- (if p > p' orelse
- (show_brackets andalso p' <> Syntax_Ext.max_pri andalso not (is_chain pr))
+ and parT m (pr, args, p, p': int) = #1 (synT m
+ (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
--- a/src/Pure/Syntax/syntax.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat Apr 09 13:10:20 2011 +0200
@@ -7,7 +7,6 @@
signature SYNTAX =
sig
- val max_pri: int
val const: string -> term
val free: string -> term
val var: indexname -> term
@@ -95,7 +94,7 @@
val pp_global: theory -> Pretty.pp
type syntax
val eq_syntax: syntax * syntax -> bool
- val is_const: syntax -> string -> bool
+ val lookup_const: syntax -> string -> string option
val is_keyword: syntax -> string -> bool
val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
val parse: Proof.context -> syntax -> string -> Lexicon.token list -> Parser.parsetree list
@@ -111,8 +110,9 @@
type mode
val mode_default: mode
val mode_input: mode
+ val empty_syntax: syntax
val merge_syntaxes: syntax -> syntax -> syntax
- val basic_syntax: syntax
+ val token_markers: string list
val basic_nonterms: string list
val print_gram: syntax -> unit
val print_trans: syntax -> unit
@@ -143,8 +143,6 @@
structure Syntax: SYNTAX =
struct
-val max_pri = Syntax_Ext.max_pri;
-
val const = Lexicon.const;
val free = Lexicon.free;
val var = Lexicon.var;
@@ -155,7 +153,7 @@
(* configuration options *)
-val root = Config.string (Config.declare "syntax_root" (K (Config.String Syntax_Ext.any)));
+val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
val positions = Config.bool positions_raw;
@@ -460,7 +458,7 @@
input: Syntax_Ext.xprod list,
lexicon: Scan.lexicon,
gram: Parser.gram,
- consts: string list,
+ consts: string Symtab.table,
prmodes: string list,
parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
parse_ruletab: ruletab,
@@ -472,7 +470,7 @@
fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
-fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
+fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt gram;
@@ -497,7 +495,7 @@
({input = [],
lexicon = Scan.empty_lexicon,
gram = Parser.empty_gram,
- consts = [],
+ consts = Symtab.empty,
prmodes = [],
parse_ast_trtab = Symtab.empty,
parse_ruletab = Symtab.empty,
@@ -510,6 +508,11 @@
(* update_syntax *)
+fun update_const (c, b) tab =
+ if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
+ then tab
+ else Symtab.update (c, b) tab;
+
fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
let
val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab,
@@ -525,7 +528,7 @@
({input = new_xprods @ input,
lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
gram = Parser.extend_gram new_xprods gram,
- consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
+ consts = fold update_const consts2 consts1,
prmodes = insert (op =) mode prmodes,
parse_ast_trtab =
update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -584,7 +587,7 @@
({input = Library.merge (op =) (input1, input2),
lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
gram = Parser.merge_gram (gram1, gram2),
- consts = sort_distinct string_ord (consts1 @ consts2),
+ consts = Symtab.merge (K true) (consts1, consts2),
prmodes = Library.merge (op =) (prmodes1, prmodes2),
parse_ast_trtab =
merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
@@ -599,13 +602,14 @@
(* basic syntax *)
-val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax;
+val token_markers =
+ ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
val basic_nonterms =
- (Lexicon.terminals @ [Syntax_Ext.logic, "type", "types", "sort", "classes",
- Syntax_Ext.args, Syntax_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
- "asms", Syntax_Ext.any, Syntax_Ext.sprop, "num_const", "float_const", "index",
- "struct", "id_position", "longid_position", "type_name", "class_name"]);
+ (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
+ "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
+ "any", "prop'", "num_const", "float_const", "index", "struct",
+ "id_position", "longid_position", "type_name", "class_name"]);
@@ -628,8 +632,8 @@
fun pretty_trans (Syntax (tabs, _)) =
let
- fun pretty_trtab name tab =
- pretty_strs_qs name (Symtab.keys tab);
+ fun pretty_tab name tab =
+ pretty_strs_qs name (sort_strings (Symtab.keys tab));
fun pretty_ruletab name tab =
Pretty.big_list name (map Ast.pretty_rule (dest_ruletab tab));
@@ -637,13 +641,13 @@
val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
print_ruletab, print_ast_trtab, ...} = tabs;
in
- [pretty_strs_qs "consts:" consts,
- pretty_trtab "parse_ast_translation:" parse_ast_trtab,
- pretty_ruletab "parse_rules:" parse_ruletab,
- pretty_trtab "parse_translation:" parse_trtab,
- pretty_trtab "print_translation:" print_trtab,
- pretty_ruletab "print_rules:" print_ruletab,
- pretty_trtab "print_ast_translation:" print_ast_trtab]
+ [pretty_tab "consts:" consts,
+ pretty_tab "parse_ast_translation:" parse_ast_trtab,
+ pretty_ruletab "parse_rules:" parse_ruletab,
+ pretty_tab "parse_translation:" parse_trtab,
+ pretty_tab "print_translation:" print_trtab,
+ pretty_ruletab "print_rules:" print_ruletab,
+ pretty_tab "print_ast_translation:" print_ast_trtab]
end;
in
--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sat Apr 09 13:10:20 2011 +0200
@@ -7,14 +7,6 @@
signature SYNTAX_EXT =
sig
val dddot_indexname: indexname
- val logic: string
- val args: string
- val cargs: string
- val typeT: typ
- val any: string
- val sprop: string
- val spropT: typ
- val max_pri: int
datatype mfix = Mfix of string * typ * string * int list * int
val err_in_mfix: string -> mfix -> 'a
val typ_to_nonterm: typ -> string
@@ -29,7 +21,7 @@
datatype syn_ext =
Syn_Ext of {
xprods: xprod list,
- consts: string list,
+ consts: (string * string) list,
parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
parse_rules: (Ast.ast * Ast.ast) list,
parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
@@ -39,19 +31,18 @@
val mfix_delims: string -> string list
val mfix_args: string -> int
val escape: string -> string
- val syn_ext': bool -> (string -> bool) -> mfix list ->
- string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
+ val syn_ext': (string -> bool) -> mfix list ->
+ (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
(Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
- val syn_ext: mfix list -> string list ->
+ val syn_ext: mfix list -> (string * string) list ->
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
(Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
- val syn_ext_const_names: string list -> syn_ext
val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
val syn_ext_trfuns:
(string * ((Ast.ast list -> Ast.ast) * stamp)) list *
@@ -66,8 +57,6 @@
val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
val mk_trfun: string * 'a -> string * ('a * stamp)
val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
- val token_markers: string list
- val pure_ext: syn_ext
end;
structure Syntax_Ext: SYNTAX_EXT =
@@ -79,24 +68,6 @@
val dddot_indexname = ("dddot", 0);
-(* syntactic categories *)
-
-val logic = "logic";
-val logicT = Type (logic, []);
-
-val args = "args";
-val cargs = "cargs";
-
-val typeT = Type ("type", []);
-
-val sprop = "#prop";
-val spropT = Type (sprop, []);
-
-val any = "any";
-val anyT = Type (any, []);
-
-
-
(** datatype xprod **)
(*Delim s: delimiter s
@@ -134,7 +105,6 @@
datatype xprod = XProd of string * xsymb list * string * int;
-val max_pri = 1000; (*maximum legal priority*)
val chain_pri = ~1; (*dummy for chain productions*)
fun delims_of xprods =
@@ -165,10 +135,10 @@
| typ_to_nt default _ = default;
(*get nonterminal for rhs*)
-val typ_to_nonterm = typ_to_nt any;
+val typ_to_nonterm = typ_to_nt "any";
(*get nonterminal for lhs*)
-val typ_to_nonterm1 = typ_to_nt logic;
+val typ_to_nonterm1 = typ_to_nt "logic";
(* read mixfix annotations *)
@@ -219,10 +189,10 @@
(* mfix_to_xprod *)
-fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
let
fun check_pri p =
- if p >= 0 andalso p <= max_pri then ()
+ if p >= 0 andalso p <= 1000 then ()
else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
fun blocks_ok [] 0 = true
@@ -255,7 +225,7 @@
| rem_pri sym = sym;
fun logify_types (a as (Argument (s, p))) =
- if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
+ if s <> "prop" andalso is_logtype s then Argument ("logic", p) else a
| logify_types a = a;
@@ -287,8 +257,9 @@
andalso not (null symbs)
andalso not (exists is_delim symbs);
val lhs' =
- if convert andalso not copy_prod then
- (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
+ if copy_prod orelse lhs = "prop" andalso symbs = [Argument ("prop'", 0)] then lhs
+ else if lhs = "prop" then "prop'"
+ else if is_logtype lhs then "logic"
else lhs;
val symbs' = map logify_types symbs;
val xprod = XProd (lhs', symbs', const', pri);
@@ -311,7 +282,7 @@
datatype syn_ext =
Syn_Ext of {
xprods: xprod list,
- consts: string list,
+ consts: (string * string) list,
parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
parse_rules: (Ast.ast * Ast.ast) list,
parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
@@ -322,19 +293,18 @@
(* syn_ext *)
-fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
let
val (parse_ast_translation, parse_translation, print_translation,
print_ast_translation) = trfuns;
- val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
+ val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes
|> split_list |> apsnd (rev o flat);
- val mfix_consts =
- distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
+ val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods;
in
Syn_Ext {
xprods = xprods,
- consts = union (op =) consts mfix_consts,
+ consts = mfix_consts @ consts,
parse_ast_translation = parse_ast_translation,
parse_rules = parse_rules' @ parse_rules,
parse_translation = parse_translation,
@@ -344,9 +314,8 @@
end;
-val syn_ext = syn_ext' true (K false);
+val syn_ext = syn_ext' (K false);
-fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
@@ -359,22 +328,4 @@
fun mk_trfun tr = stamp_trfun (stamp ()) tr;
fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
-
-(* pure_ext *)
-
-val token_markers =
- ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
-
-val pure_ext = syn_ext' false (K false)
- [Mfix ("_", spropT --> propT, "", [0], 0),
- Mfix ("_", logicT --> anyT, "", [0], 0),
- Mfix ("_", spropT --> anyT, "", [0], 0),
- Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
- Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
- Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
- Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
- token_markers
- ([], [], [], [])
- ([], []);
-
end;
--- a/src/Pure/Syntax/syntax_phases.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Apr 09 13:10:20 2011 +0200
@@ -18,6 +18,40 @@
structure Syntax_Phases: SYNTAX_PHASES =
struct
+(** markup logical entities **)
+
+fun markup_class ctxt c =
+ [Name_Space.markup_entry (Type.class_space (ProofContext.tsig_of ctxt)) c];
+
+fun markup_type ctxt c =
+ [Name_Space.markup_entry (Type.type_space (ProofContext.tsig_of ctxt)) c];
+
+fun markup_const ctxt c =
+ [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
+
+fun markup_free ctxt x =
+ [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
+ (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
+ else [Markup.hilite]);
+
+fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
+
+fun markup_bound def id =
+ [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
+
+fun markup_entity ctxt c =
+ (case Syntax.lookup_const (ProofContext.syn_of ctxt) c of
+ SOME "" => []
+ | SOME b => markup_entity ctxt b
+ | NONE => c |> Lexicon.unmark
+ {case_class = markup_class ctxt,
+ case_type = markup_type ctxt,
+ case_const = markup_const ctxt,
+ case_fixed = markup_free ctxt,
+ case_default = K []});
+
+
+
(** decode parse trees **)
(* sort_of_term *)
@@ -89,29 +123,10 @@
(* parsetree_to_ast *)
-fun markup_const ctxt c =
- [Name_Space.markup_entry (Consts.space_of (ProofContext.consts_of ctxt)) c];
-
-fun markup_free ctxt x =
- [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
- (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
- else [Markup.hilite]);
-
fun parsetree_to_ast ctxt constrain_pos trf parsetree =
let
- val tsig = ProofContext.tsig_of ctxt;
-
val get_class = ProofContext.read_class ctxt;
val get_type = #1 o dest_Type o ProofContext.read_type_name_proper ctxt false;
- fun markup_class c = [Name_Space.markup_entry (Type.class_space tsig) c];
- fun markup_type c = [Name_Space.markup_entry (Type.type_space tsig) c];
-
- val markup_entity = Lexicon.unmark
- {case_class = markup_class,
- case_type = markup_type,
- case_const = markup_const ctxt,
- case_fixed = markup_free ctxt,
- case_default = K []};
val reports = Unsynchronized.ref ([]: Position.reports);
fun report pos = Position.reports reports [pos];
@@ -124,12 +139,12 @@
fun asts_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
let
val c = get_class (Lexicon.str_of_token tok);
- val _ = report (Lexicon.pos_of_token tok) markup_class c;
+ val _ = report (Lexicon.pos_of_token tok) (markup_class ctxt) c;
in [Ast.Constant (Lexicon.mark_class c)] end
| asts_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
let
val c = get_type (Lexicon.str_of_token tok);
- val _ = report (Lexicon.pos_of_token tok) markup_type c;
+ val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
if constrain_pos then
@@ -141,7 +156,7 @@
val _ = pts |> List.app
(fn Parser.Node _ => () | Parser.Tip tok =>
if Lexicon.valued_token tok then ()
- else report (Lexicon.pos_of_token tok) markup_entity a);
+ else report (Lexicon.pos_of_token tok) (markup_entity ctxt) a);
in [trans a (maps asts_of pts)] end
| asts_of (Parser.Tip tok) =
if Lexicon.valued_token tok
@@ -185,9 +200,6 @@
((true, #1 (Term.dest_Const (ProofContext.read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (ProofContext.consts_of ctxt) a));
val get_free = ProofContext.intern_skolem ctxt;
- fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
- fun markup_bound def id =
- [Markup.properties [(if def then Markup.defN else Markup.refN, id)] Markup.bound];
val decodeT = typ_of_term (ProofContext.get_sort ctxt (term_sorts tm));
@@ -390,7 +402,8 @@
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
- if Syntax.is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
+ if is_some (Syntax.lookup_const syn x) orelse Long_Name.is_qualified x
+ then Ast.Constant x
else ast
| constify (Ast.Appl asts) = Ast.Appl (map constify asts);
@@ -491,7 +504,7 @@
val {structs, fixes} = idents;
fun mark_atoms ((t as Const (c, _)) $ u) =
- if member (op =) Syntax_Ext.token_markers c
+ if member (op =) Syntax.token_markers c
then t $ u else mark_atoms t $ mark_atoms u
| mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
| mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
@@ -602,12 +615,16 @@
| token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
| token_trans _ _ = NONE;
- val markup_extern = Lexicon.unmark
- {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
- case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
- case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
- case_fixed = fn x => free_or_skolem ctxt x,
- case_default = fn x => ([], x)};
+ fun markup_extern c =
+ (case Syntax.lookup_const syn c of
+ SOME "" => ([], c)
+ | SOME b => markup_extern b
+ | NONE => c |> Lexicon.unmark
+ {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
+ case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
+ case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
+ case_fixed = fn x => free_or_skolem ctxt x,
+ case_default = fn x => ([], x)});
in
t_to_ast ctxt (Syntax.print_translation syn) t
|> Ast.normalize ctxt (Syntax.print_rules syn)
@@ -626,7 +643,7 @@
val syn = ProofContext.syn_of ctxt;
val idents = Local_Syntax.idents_of (ProofContext.syntax_of ctxt);
in
- unparse_t (term_to_ast idents (Syntax.is_const syn))
+ unparse_t (term_to_ast idents (is_some o Syntax.lookup_const syn))
(Printer.pretty_term_ast (not (Pure_Thy.old_appl_syntax thy)))
Markup.term ctxt
end;
@@ -660,10 +677,25 @@
| type_constraint_tr' _ _ _ = raise Match;
+(* authentic syntax *)
+
+fun const_ast_tr intern ctxt [Ast.Variable c] =
+ let
+ val Const (c', _) = ProofContext.read_const_proper ctxt false c;
+ val d = if intern then Lexicon.mark_const c' else c;
+ in Ast.Constant d end
+ | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T]] =
+ Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
+ | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
+
+
(* setup translations *)
val _ = Context.>> (Context.map_theory
- (Sign.add_advanced_trfunsT
+ (Sign.add_advanced_trfuns
+ ([("_context_const", const_ast_tr true),
+ ("_context_xconst", const_ast_tr false)], [], [], []) #>
+ Sign.add_advanced_trfunsT
[("_type_prop", type_prop_tr'),
("\\<^const>TYPE", type_tr'),
("_type_constraint_", type_constraint_tr')]));
--- a/src/Pure/pure_thy.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/pure_thy.ML Sat Apr 09 13:10:20 2011 +0200
@@ -19,9 +19,6 @@
val tycon = Lexicon.mark_type;
val const = Lexicon.mark_const;
-val typeT = Syntax_Ext.typeT;
-val spropT = Syntax_Ext.spropT;
-
(* application syntax variants *)
@@ -64,15 +61,23 @@
(Binding.name "itself", 1, NoSyn),
(Binding.name "dummy", 0, NoSyn)]
#> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
+ #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
#> Sign.add_syntax_i
- [("", typ "tid => type", Delimfix "_"),
+ [("", typ "prop' => prop", Delimfix "_"),
+ ("", typ "logic => any", Delimfix "_"),
+ ("", typ "prop' => any", Delimfix "_"),
+ ("", typ "logic => logic", Delimfix "'(_')"),
+ ("", typ "prop' => prop'", Delimfix "'(_')"),
+ ("_constrain", typ "logic => type => logic", Mixfix ("_::_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_::_", [4, 0], 3)),
+ ("", typ "tid => type", Delimfix "_"),
("", typ "tvar => type", Delimfix "_"),
("", typ "type_name => type", Delimfix "_"),
("_type_name", typ "id => type_name", Delimfix "_"),
("_type_name", typ "longid => type_name", Delimfix "_"),
- ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
- ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
- ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], Syntax.max_pri)),
+ ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
+ ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
+ ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], 1000)),
("", typ "class_name => sort", Delimfix "_"),
("_class_name", typ "id => class_name", Delimfix "_"),
("_class_name", typ "longid => class_name", Delimfix "_"),
@@ -80,7 +85,7 @@
("_sort", typ "classes => sort", Delimfix "{_}"),
("", typ "class_name => classes", Delimfix "_"),
("_classes", typ "class_name => classes => classes", Delimfix "_,_"),
- ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [Syntax.max_pri, 0], Syntax.max_pri)),
+ ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [1000, 0], 1000)),
("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
("", typ "type => types", Delimfix "_"),
("_types", typ "type => types => types", Delimfix "_,/ _"),
@@ -128,10 +133,18 @@
("_indexvar", typ "index", Delimfix "'\\<index>"),
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("_update_name", typ "idt", NoSyn),
- ("_constrainAbs", typ "'a", NoSyn),
+ ("_constrainAbs", typ "'a", NoSyn),
("_constrain_position", typ "id => id_position", Delimfix "_"),
("_constrain_position", typ "longid => longid_position", Delimfix "_"),
("_type_constraint_", typ "'a", NoSyn),
+ ("_context_const", typ "id_position => logic", Delimfix "CONST _"),
+ ("_context_const", typ "id_position => aprop", Delimfix "CONST _"),
+ ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
+ ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
+ ("_context_xconst", typ "id_position => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "id_position => aprop", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
+ ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
(const "==>", typ "prop => prop => prop", Delimfix "op ==>"),
(const Term.dummy_patternN, typ "aprop", Delimfix "'_"),
("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
@@ -143,7 +156,7 @@
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
--- a/src/Pure/sign.ML Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Pure/sign.ML Sat Apr 09 13:10:20 2011 +0200
@@ -140,7 +140,7 @@
make_sign (Name_Space.default_naming, syn, tsig, consts);
val empty =
- make_sign (Name_Space.default_naming, Syntax.basic_syntax, Type.empty_tsig, Consts.empty);
+ make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
fun merge pp (sign1, sign2) =
let
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Fri Apr 08 19:04:08 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Sat Apr 09 13:10:20 2011 +0200
@@ -69,16 +69,6 @@
/* markup selectors */
- private val subexp_include =
- Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
- Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR)
-
- val subexp: Markup_Tree.Select[(Text.Range, Color)] =
- {
- case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
- (range, Color.black)
- }
-
val message: Markup_Tree.Select[Color] =
{
case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
@@ -125,6 +115,19 @@
case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)"
case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)"
case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable"
+ case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable"
+ case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable"
+ }
+
+ private val subexp_include =
+ Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+ Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
+ Markup.TFREE, Markup.TVAR)
+
+ val subexp: Markup_Tree.Select[(Text.Range, Color)] =
+ {
+ case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ (range, Color.black)
}