--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Mon Apr 04 16:35:46 2011 +0200
@@ -464,13 +464,13 @@
if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
val case_constant = Constant (syntax (case_const dummyT))
fun case_trans authentic =
- (if authentic then ParsePrintRule else ParseRule)
+ (if authentic then Parse_Print_Rule else Parse_Rule)
(app "_case_syntax"
(Variable "x",
foldr1 (app "_case2") (map_index (case1 authentic) spec)),
capp (capps (case_constant, map_index arg1 spec), Variable "x"))
fun one_abscon_trans authentic (n, c) =
- (if authentic then ParsePrintRule else ParseRule)
+ (if authentic then Parse_Print_Rule else Parse_Rule)
(cabs (con1 authentic n c, expvar n),
capps (case_constant, map_index (when1 n) spec))
fun abscon_trans authentic =
@@ -479,7 +479,7 @@
case_trans false :: case_trans true ::
abscon_trans false @ abscon_trans true
in
- val thy = Sign.add_trrules_i trans_rules thy
+ val thy = Sign.add_trrules trans_rules thy
end
(* prove beta reduction rule for case combinator *)
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Mon Apr 04 16:35:46 2011 +0200
@@ -24,9 +24,9 @@
fun trans_rules name2 name1 n mx =
let
val vnames = Name.invents Name.context "a" n
- val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1)
+ val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
in
- [Syntax.ParsePrintRule
+ [Syntax.Parse_Print_Rule
(Syntax.mk_appl (Constant name2) (map Variable vnames),
fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
vnames (Constant name1))] @
@@ -80,7 +80,7 @@
in
thy
|> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
- |> Sign.add_trrules_i (maps #3 transformed_decls)
+ |> Sign.add_trrules (maps #3 transformed_decls)
end
in
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Mon Apr 04 16:28:36 2011 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Mon Apr 04 16:35:46 2011 +0200
@@ -516,17 +516,17 @@
val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
in
- [ParseRule (app_pat (capps (cname, xs)),
+ [Parse_Rule (app_pat (capps (cname, xs)),
mk_appl pname (map app_pat xs)),
- ParseRule (app_var (capps (cname, xs)),
+ Parse_Rule (app_var (capps (cname, xs)),
app_var (args_list xs)),
- PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
+ Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
app "_match" (mk_appl pname ps, args_list vs))]
end;
val trans_rules : Syntax.ast Syntax.trrule list =
maps one_case_trans (pat_consts ~~ spec);
in
- val thy = Sign.add_trrules_i trans_rules thy;
+ val thy = Sign.add_trrules trans_rules thy;
end;
(* prove strictness and reduction rules of pattern combinators *)
--- a/src/Pure/General/markup.scala Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/General/markup.scala Mon Apr 04 16:35:46 2011 +0200
@@ -97,6 +97,19 @@
val DEF = "def"
val REF = "ref"
+ object Entity
+ {
+ def unapply(markup: Markup): Option[(String, String)] =
+ markup match {
+ case Markup(ENTITY, props @ Kind(kind)) =>
+ props match {
+ case Name(name) => Some(kind, name)
+ case _ => None
+ }
+ case _ => None
+ }
+ }
+
/* position */
--- a/src/Pure/General/position.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/General/position.ML Mon Apr 04 16:35:46 2011 +0200
@@ -34,6 +34,8 @@
val reported_text: T -> Markup.T -> string -> string
val report_text: T -> Markup.T -> string -> unit
val report: T -> Markup.T -> unit
+ type reports = (T * Markup.T) list
+ val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
val str_of: T -> string
type range = T * T
val no_range: range
@@ -155,6 +157,13 @@
fun report_text pos markup txt = Output.report (reported_text pos markup txt);
fun report pos markup = report_text pos markup "";
+type reports = (T * Markup.T) list;
+
+fun reports _ [] _ _ = ()
+ | reports (r: reports Unsynchronized.ref) ps markup x =
+ let val ms = markup x
+ in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
+
(* str_of *)
--- a/src/Pure/Isar/isar_cmd.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Apr 04 16:35:46 2011 +0200
@@ -13,6 +13,8 @@
val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+ val translations: (xstring * string) Syntax.trrule list -> theory -> theory
+ val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
val add_axioms: (Attrib.binding * string) list -> theory -> theory
val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
@@ -154,6 +156,22 @@
end;
+(* translation rules *)
+
+fun read_trrules thy raw_rules =
+ let
+ val ctxt = ProofContext.init_global thy;
+ val type_ctxt = ProofContext.type_context ctxt;
+ val syn = ProofContext.syn_of ctxt;
+ in
+ raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
+ Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s)))
+ end;
+
+fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
+fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
+
+
(* oracles *)
fun oracle (name, pos) (body_txt, body_pos) =
--- a/src/Pure/Isar/isar_syn.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Apr 04 16:35:46 2011 +0200
@@ -175,9 +175,9 @@
-- Parse.string;
fun trans_arrow toks =
- ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
- (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
- (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
+ ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
+ (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
+ (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
val trans_line =
trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
@@ -185,11 +185,11 @@
val _ =
Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
- (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
+ (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
val _ =
Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
- (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
+ (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
(* axioms and definitions *)
--- a/src/Pure/Isar/proof_context.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Apr 04 16:35:46 2011 +0200
@@ -65,7 +65,9 @@
val allow_dummies: Proof.context -> Proof.context
val check_tvar: Proof.context -> indexname * sort -> indexname * sort
val check_tfree: Proof.context -> string * sort -> string * sort
- val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term
+ val type_context: Proof.context -> Syntax.type_context
+ val term_context: Proof.context -> Syntax.term_context
+ val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
val standard_infer_types: Proof.context -> term list -> term list
val read_term_pattern: Proof.context -> string -> term
val read_term_schematic: Proof.context -> string -> term
@@ -665,12 +667,18 @@
in
+fun type_context ctxt : Syntax.type_context =
+ {get_class = read_class ctxt,
+ get_type = #1 o dest_Type o read_type_name_proper ctxt false,
+ markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
+ markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
+
fun term_context ctxt : Syntax.term_context =
{get_sort = get_sort ctxt,
get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
get_free = intern_skolem ctxt (Variable.def_type ctxt false),
- markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x],
+ markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
markup_free = fn 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]),
@@ -748,14 +756,16 @@
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
- val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
+ val S =
+ Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos)
handle ERROR msg => parse_failed ctxt pos msg "sort";
in Type.minimize_sort (tsig_of ctxt) S end;
fun parse_typ ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
- val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
+ val T =
+ Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos)
handle ERROR msg => parse_failed ctxt pos msg "type";
in T end;
@@ -777,8 +787,9 @@
fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
handle ERROR msg => SOME msg;
val t =
- Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos)
- handle ERROR msg => parse_failed ctxt pos msg kind;
+ Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
+ root (syms, pos)
+ handle ERROR msg => parse_failed ctxt pos msg kind;
in t end;
@@ -1079,13 +1090,6 @@
(* authentic syntax *)
-val _ = Context.>>
- (Context.map_theory
- (Sign.add_advanced_trfuns
- (Syntax.type_ast_trs
- {read_class = read_class,
- read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
-
local
fun const_ast_tr intern ctxt [Syntax.Variable c] =
--- a/src/Pure/Proof/proof_syntax.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Mon Apr 04 16:35:46 2011 +0200
@@ -70,7 +70,7 @@
(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
+ |> Sign.add_trrules (map Syntax.Parse_Print_Rule
[(Syntax.mk_appl (Constant "_Lam")
[Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
Syntax.mk_appl (Constant "_Lam")
--- a/src/Pure/Syntax/parser.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Syntax/parser.ML Mon Apr 04 16:35:46 2011 +0200
@@ -15,6 +15,7 @@
datatype parsetree =
Node of string * parsetree list |
Tip of Lexicon.token
+ val pretty_parsetree: parsetree -> Pretty.T
val parse: Proof.context -> gram -> string -> Lexicon.token list -> parsetree list
val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
val branching_level: int Config.T
@@ -632,6 +633,11 @@
Node of string * parsetree list |
Tip of Lexicon.token;
+fun pretty_parsetree (Node (c, pts)) =
+ Pretty.enclose "(" ")" (Pretty.breaks
+ (Pretty.quote (Pretty.str c) :: map pretty_parsetree pts))
+ | pretty_parsetree (Tip tok) = Pretty.str (Lexicon.str_of_token tok);
+
type state =
nt_tag * int * (*identification and production precedence*)
parsetree list * (*already parsed nonterminals on rhs*)
--- a/src/Pure/Syntax/syn_trans.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Mon Apr 04 16:35:46 2011 +0200
@@ -48,6 +48,7 @@
(string * (term list -> term)) list *
(string * (bool -> typ -> term list -> term)) list *
(string * (Ast.ast list -> Ast.ast)) list
+ type type_context
end;
signature SYN_TRANS =
@@ -57,8 +58,9 @@
val prop_tr': term -> term
val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
- val parsetree_to_ast: Proof.context -> bool ->
- (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
+ val parsetree_to_ast: Proof.context -> type_context -> bool ->
+ (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
+ Parser.parsetree -> Position.reports * Ast.ast
val ast_to_term: Proof.context ->
(string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
end;
@@ -549,21 +551,44 @@
(** parsetree_to_ast **)
-fun parsetree_to_ast ctxt constrain_pos trf =
+type type_context =
+ {get_class: string -> string,
+ get_type: string -> string,
+ markup_class: string -> Markup.T list,
+ markup_type: string -> Markup.T list};
+
+fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree =
let
+ val {get_class, get_type, markup_class, markup_type} = type_context;
+
+ val reports = Unsynchronized.ref ([]: Position.reports);
+ fun report pos = Position.reports reports [pos];
+
fun trans a args =
(case trf a of
NONE => Ast.mk_appl (Ast.Constant a) args
| SOME f => f ctxt args);
- fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
+ fun ast_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;
+ in Ast.Constant (Lexicon.mark_class c) end
+ | ast_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;
+ in Ast.Constant (Lexicon.mark_type c) end
+ | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
if constrain_pos then
Ast.Appl [Ast.Constant "_constrain", ast_of pt,
Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
else ast_of pt
| ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
| ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
- in ast_of end;
+
+ val ast = ast_of parsetree;
+ in (! reports, ast) end;
--- a/src/Pure/Syntax/syntax.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Apr 04 16:35:46 2011 +0200
@@ -116,17 +116,20 @@
val ambiguity_level_raw: Config.raw
val ambiguity_level: int Config.T
val ambiguity_limit: int Config.T
- val standard_parse_term: (term -> string option) -> term_context ->
- Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term
- val standard_parse_typ: Proof.context -> syntax ->
+ val standard_parse_term: (term -> string option) ->
+ Proof.context -> type_context -> term_context -> syntax ->
+ string -> Symbol_Pos.T list * Position.T -> term
+ val standard_parse_typ: Proof.context -> type_context -> syntax ->
((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
- val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
+ val standard_parse_sort: Proof.context -> type_context -> syntax ->
+ Symbol_Pos.T list * Position.T -> sort
datatype 'a trrule =
- ParseRule of 'a * 'a |
- PrintRule of 'a * 'a |
- ParsePrintRule of 'a * 'a
+ Parse_Rule of 'a * 'a |
+ Print_Rule of 'a * 'a |
+ Parse_Print_Rule of 'a * 'a
val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
val is_const: syntax -> string -> bool
+ val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
val standard_unparse_term: {structs: string list, fixes: string list} ->
{extern_class: string -> xstring, extern_type: string -> xstring,
extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
@@ -149,10 +152,8 @@
val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
val update_const_gram: bool -> (string -> bool) ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
- val update_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
- val remove_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
- val update_trrules_i: ast trrule list -> syntax -> syntax
- val remove_trrules_i: ast trrule list -> syntax -> syntax
+ val update_trrules: ast trrule list -> syntax -> syntax
+ val remove_trrules: ast trrule list -> syntax -> syntax
end;
structure Syntax: SYNTAX =
@@ -619,8 +620,8 @@
val basic_nonterms =
(Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
- "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
- "index", "struct", "id_position", "longid_position"]);
+ "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index",
+ "struct", "id_position", "longid_position", "type_name", "class_name"]);
@@ -711,7 +712,7 @@
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) =
+fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
let
val {lexicon, gram, parse_ast_trtab, ...} = tabs;
val toks = Lexicon.tokenize lexicon raw syms;
@@ -724,8 +725,6 @@
val len = length pts;
val limit = Config.get ctxt ambiguity_limit;
- fun show_pt pt =
- Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt));
val _ =
if len <= Config.get ctxt ambiguity_level then ()
else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
@@ -734,21 +733,22 @@
(("Ambiguous input" ^ Position.str_of pos ^
"\nproduces " ^ string_of_int len ^ " parse trees" ^
(if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map show_pt (take limit pts))));
+ map (Pretty.string_of o Parser.pretty_parsetree) (take limit pts))));
val constrain_pos = not raw andalso Config.get ctxt positions;
in
- some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
+ some_results
+ (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
end;
(* read *)
-fun read ctxt (syn as Syntax (tabs, _)) root inp =
+fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
let val {parse_ruletab, parse_trtab, ...} = tabs in
- read_asts ctxt syn false root inp
- |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab))
- |> some_results (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab))
+ read_asts ctxt type_ctxt syn false root inp
+ |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
+ |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
end;
@@ -790,51 +790,60 @@
map (show_term o snd) (take limit results)))
end;
-fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) =
- read ctxt syn root (syms, pos)
+fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
+ read ctxt type_ctxt syn root (syms, pos)
|> map (Type_Ext.decode_term term_ctxt)
|> disambig ctxt check;
(* read types *)
-fun standard_parse_typ ctxt syn get_sort (syms, pos) =
- (case read ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
- [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
+fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
+ (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
+ [res] =>
+ let val t = report_result ctxt res
+ in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
| _ => error (ambiguity_msg pos));
(* read sorts *)
-fun standard_parse_sort ctxt syn (syms, pos) =
- (case read ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
- [t] => Type_Ext.sort_of_term t
+fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
+ (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
+ [res] =>
+ let val t = report_result ctxt res
+ in Type_Ext.sort_of_term t end
| _ => error (ambiguity_msg pos));
(** prepare translation rules **)
+(* rules *)
+
datatype 'a trrule =
- ParseRule of 'a * 'a |
- PrintRule of 'a * 'a |
- ParsePrintRule of 'a * 'a;
+ Parse_Rule of 'a * 'a |
+ Print_Rule of 'a * 'a |
+ Parse_Print_Rule of 'a * 'a;
-fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
- | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
- | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
+fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y)
+ | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y)
+ | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y);
-fun parse_rule (ParseRule pats) = SOME pats
- | parse_rule (PrintRule _) = NONE
- | parse_rule (ParsePrintRule pats) = SOME pats;
+fun parse_rule (Parse_Rule pats) = SOME pats
+ | parse_rule (Print_Rule _) = NONE
+ | parse_rule (Parse_Print_Rule pats) = SOME pats;
-fun print_rule (ParseRule _) = NONE
- | print_rule (PrintRule pats) = SOME (swap pats)
- | print_rule (ParsePrintRule pats) = SOME (swap pats);
+fun print_rule (Parse_Rule _) = NONE
+ | print_rule (Print_Rule pats) = SOME (swap pats)
+ | print_rule (Parse_Print_Rule pats) = SOME (swap pats);
fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
+
+(* check_rules *)
+
local
fun check_rule rule =
@@ -844,7 +853,18 @@
Pretty.string_of (Ast.pretty_rule rule))
| NONE => rule);
-fun read_pattern ctxt syn (root, str) =
+in
+
+fun check_rules rules =
+ (map check_rule (map_filter parse_rule rules),
+ map check_rule (map_filter print_rule rules));
+
+end;
+
+
+(* read_rule_pattern *)
+
+fun read_rule_pattern ctxt type_ctxt syn (root, str) =
let
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
@@ -854,25 +874,13 @@
val (syms, pos) = read_token str;
in
- (case read_asts ctxt syn true root (syms, pos) of
- [ast] => constify ast
+ (case read_asts ctxt type_ctxt syn true root (syms, pos) of
+ [res] =>
+ let val ast = report_result ctxt res
+ in constify ast end
| _ => error (ambiguity_msg pos))
end;
-fun prep_rules rd_pat raw_rules =
- let val rules = map (map_trrule rd_pat) raw_rules in
- (map check_rule (map_filter parse_rule rules),
- map check_rule (map_filter print_rule rules))
- end
-
-in
-
-val cert_rules = prep_rules I;
-
-fun read_rules ctxt syn = prep_rules (read_pattern ctxt syn);
-
-end;
-
(** unparse terms, typs, sorts **)
@@ -920,14 +928,8 @@
fun update_const_gram add is_logtype prmode decls =
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
-fun update_trrules ctxt syn =
- ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt syn;
-
-fun remove_trrules ctxt syn =
- remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt syn;
-
-val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
-val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
+val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules;
+val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules;
(*export parts of internal Syntax structures*)
--- a/src/Pure/Syntax/type_ext.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/Syntax/type_ext.ML Mon Apr 04 16:35:46 2011 +0200
@@ -13,14 +13,10 @@
val strip_positions: term -> term
val strip_positions_ast: Ast.ast -> Ast.ast
type term_context
- val decode_term: term_context -> term -> (Position.T * Markup.T) list * term
+ val decode_term: term_context -> Position.reports * term -> Position.reports * term
val term_of_typ: bool -> typ -> term
val no_brackets: unit -> bool
val no_type_brackets: unit -> bool
- val type_ast_trs:
- {read_class: Proof.context -> string -> string,
- read_type: Proof.context -> string -> string} ->
- (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
end;
signature TYPE_EXT =
@@ -140,16 +136,13 @@
markup_free: string -> Markup.T list,
markup_var: indexname -> Markup.T list};
-fun decode_term (term_context: term_context) tm =
+fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
let
val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
val decodeT = typ_of_term (get_sort (term_sorts tm));
- val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
- fun report [] _ _ = ()
- | report ps markup x =
- let val ms = markup x
- in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
+ val reports = Unsynchronized.ref reports0;
+ fun report ps = Position.reports reports ps;
fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
(case decode_position typ of
@@ -252,30 +245,14 @@
(* parse ast translations *)
-val class_ast = Ast.Constant o Lexicon.mark_class;
-val type_ast = Ast.Constant o Lexicon.mark_type;
-
-fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
- | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
-
-fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
- Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
- | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
+fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
+ | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
-fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
- | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
-
-fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
- Ast.Appl [type_ast (read_type c), ty]
- | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
+fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
+ | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
-fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
- Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
- | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
-
-fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
- Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
- | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
+fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
+ | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
(* print ast translations *)
@@ -296,32 +273,35 @@
(* type_ext *)
-val sortT = Type ("sort", []);
-val classesT = Type ("classes", []);
-val typesT = Type ("types", []);
+fun typ c = Type (c, []);
+
+val class_nameT = typ "class_name";
+val type_nameT = typ "type_name";
+
+val sortT = typ "sort";
+val classesT = typ "classes";
+val typesT = typ "types";
local open Lexicon Syn_Ext in
val type_ext = syn_ext' false (K false)
[Mfix ("_", tidT --> typeT, "", [], max_pri),
Mfix ("_", tvarT --> typeT, "", [], max_pri),
- Mfix ("_", idT --> typeT, "_type_name", [], max_pri),
- Mfix ("_", longidT --> typeT, "_type_name", [], max_pri),
+ Mfix ("_", type_nameT --> typeT, "", [], max_pri),
+ Mfix ("_", idT --> type_nameT, "_type_name", [], max_pri),
+ Mfix ("_", longidT --> type_nameT, "_type_name", [], max_pri),
Mfix ("_::_", [tidT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("_::_", [tvarT, sortT] ---> typeT, "_ofsort", [max_pri, 0], max_pri),
Mfix ("'_()::_", sortT --> typeT, "_dummy_ofsort", [0], max_pri),
- Mfix ("_", idT --> sortT, "_class_name", [], max_pri),
- Mfix ("_", longidT --> sortT, "_class_name", [], max_pri),
+ Mfix ("_", class_nameT --> sortT, "", [], max_pri),
+ Mfix ("_", idT --> class_nameT, "_class_name", [], max_pri),
+ Mfix ("_", longidT --> class_nameT, "_class_name", [], max_pri),
Mfix ("{}", sortT, "_topsort", [], max_pri),
Mfix ("{_}", classesT --> sortT, "_sort", [], max_pri),
- Mfix ("_", idT --> classesT, "_class_name", [], max_pri),
- Mfix ("_", longidT --> classesT, "_class_name", [], max_pri),
- Mfix ("_,_", [idT, classesT] ---> classesT, "_classes", [], max_pri),
- Mfix ("_,_", [longidT, classesT] ---> classesT, "_classes", [], max_pri),
- Mfix ("_ _", [typeT, idT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
- Mfix ("_ _", [typeT, longidT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
- Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
- Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
+ Mfix ("_", class_nameT --> classesT, "", [], max_pri),
+ Mfix ("_,_", [class_nameT, classesT] ---> classesT, "_classes", [], max_pri),
+ Mfix ("_ _", [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
+ Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri),
Mfix ("_", typeT --> typesT, "", [], max_pri),
Mfix ("_,/ _", [typeT, typesT] ---> typesT, "_types", [], max_pri),
Mfix ("(_/ => _)", [typeT, typeT] ---> typeT, "\\<^type>fun", [1, 0], 0),
@@ -329,18 +309,12 @@
Mfix ("'(_')", typeT --> typeT, "", [0], max_pri),
Mfix ("'_", typeT, "\\<^type>dummy", [], max_pri)]
["_type_prop"]
- ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
+ (map Syn_Ext.mk_trfun
+ [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
+ [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
[]
([], []);
-fun type_ast_trs {read_class, read_type} =
- [("_class_name", class_name_tr o read_class),
- ("_classes", classes_tr o read_class),
- ("_type_name", type_name_tr o read_type),
- ("_tapp", tapp_ast_tr o read_type),
- ("_tappl", tappl_ast_tr o read_type),
- ("_bracket", K bracket_ast_tr)];
-
end;
end;
--- a/src/Pure/sign.ML Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Pure/sign.ML Mon Apr 04 16:35:46 2011 +0200
@@ -108,10 +108,8 @@
(string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
-> theory -> theory
- val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
- val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
- val add_trrules_i: ast Syntax.trrule list -> theory -> theory
- val del_trrules_i: ast Syntax.trrule list -> theory -> theory
+ val add_trrules: ast Syntax.trrule list -> theory -> theory
+ val del_trrules: ast Syntax.trrule list -> theory -> theory
val new_group: theory -> theory
val reset_group: theory -> theory
val add_path: string -> theory -> theory
@@ -497,14 +495,8 @@
(* translation rules *)
-fun gen_trrules f args thy = thy |> map_syn (fn syn =>
- let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
- in f (ProofContext.init_global thy) syn rules syn end);
-
-val add_trrules = gen_trrules Syntax.update_trrules;
-val del_trrules = gen_trrules Syntax.remove_trrules;
-val add_trrules_i = map_syn o Syntax.update_trrules_i;
-val del_trrules_i = map_syn o Syntax.remove_trrules_i;
+val add_trrules = map_syn o Syntax.update_trrules;
+val del_trrules = map_syn o Syntax.remove_trrules;
(* naming *)
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Mon Apr 04 16:28:36 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Mon Apr 04 16:35:46 2011 +0200
@@ -70,7 +70,8 @@
/* markup selectors */
private val subexp_include =
- Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE)
+ 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)] =
{
@@ -111,6 +112,7 @@
val tooltip: Markup_Tree.Select[String] =
{
+ case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + name
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
margin = Isabelle.Int_Property("tooltip-margin"))
@@ -119,6 +121,10 @@
case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
+ case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)"
+ 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"
}