# HG changeset patch # User wenzelm # Date 1302347420 -7200 # Node ID 941627f5477ad905f863c2c4a3faa5bbfaa44ccb # Parent ab5747d44120c82fea6827f0c688a74602148e02# Parent 5786aa4a984096908cc65218dcf8752cc202ecf7 merged diff -r ab5747d44120 -r 941627f5477a doc-src/Codegen/Thy/Setup.thy --- 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 ("_\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end *} diff -r ab5747d44120 -r 941627f5477a src/FOL/IFOL.thy --- 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 diff -r ab5747d44120 -r 941627f5477a src/HOL/Imperative_HOL/Overview.thy --- 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 ("_\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end *}(*>*) diff -r ab5747d44120 -r 941627f5477a src/HOL/Library/OptionalSugar.thy --- 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 ("_\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end *} @@ -70,10 +68,10 @@ val classesT = Type ("classes", []); (*FIXME*) in Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_topsort", sortT, Mixfix ("\", [], Syntax.max_pri)), - ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)), - ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)), - ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)) + ("_topsort", sortT, Mixfix ("\", [], 1000)), + ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)), + ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \ _", [], 1000)), + ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \ _", [], 1000)) ] end *} diff -r ab5747d44120 -r 941627f5477a src/HOL/Tools/Datatype/datatype_data.ML --- 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)) :: diff -r ab5747d44120 -r 941627f5477a src/Pure/Isar/isar_syn.ML --- 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 = diff -r ab5747d44120 -r 941627f5477a src/Pure/Isar/parse.ML --- 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); diff -r ab5747d44120 -r 941627f5477a src/Pure/Isar/proof_context.ML --- 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 diff -r ab5747d44120 -r 941627f5477a src/Pure/ML/ml_antiquote.ML --- 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" diff -r ab5747d44120 -r 941627f5477a src/Pure/Syntax/mixfix.ML --- 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; diff -r ab5747d44120 -r 941627f5477a src/Pure/Syntax/printer.ML --- 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)) diff -r ab5747d44120 -r 941627f5477a src/Pure/Syntax/syntax.ML --- 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 diff -r ab5747d44120 -r 941627f5477a src/Pure/Syntax/syntax_ext.ML --- 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; diff -r ab5747d44120 -r 941627f5477a src/Pure/Syntax/syntax_phases.ML --- 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')])); diff -r ab5747d44120 -r 941627f5477a src/Pure/pure_thy.ML --- 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 "'\\"), ("_struct", typ "index => logic", Mixfix ("\\_", [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 ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\_", [4, 0], 3)), ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), diff -r ab5747d44120 -r 941627f5477a src/Pure/sign.ML --- 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 diff -r ab5747d44120 -r 941627f5477a src/Tools/jEdit/src/jedit/isabelle_markup.scala --- 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) }