added Position.reports convenience;
authorwenzelm
Sun Apr 03 21:59:33 2011 +0200 (2011-04-03)
changeset 42204b3277168c1e7
parent 42203 9c9c97a5040d
child 42205 22f5cc06c419
added Position.reports convenience;
modernized Syntax.trrule constructors;
modernized Sign.add_trrules/del_trrules: internal arguments;
modernized Isar_Cmd.translations/no_translations: external arguments;
explicit syntax categories class_name/type_name, with reports via type_context;
eliminated former class_name/type_name ast translations;
tuned signatures;
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/Pure/General/position.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
src/Pure/sign.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Apr 03 18:17:21 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Sun Apr 03 21:59:33 2011 +0200
     1.3 @@ -464,13 +464,13 @@
     1.4            if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
     1.5        val case_constant = Constant (syntax (case_const dummyT))
     1.6        fun case_trans authentic =
     1.7 -          (if authentic then ParsePrintRule else ParseRule)
     1.8 +          (if authentic then Parse_Print_Rule else Parse_Rule)
     1.9              (app "_case_syntax"
    1.10                (Variable "x",
    1.11                 foldr1 (app "_case2") (map_index (case1 authentic) spec)),
    1.12               capp (capps (case_constant, map_index arg1 spec), Variable "x"))
    1.13        fun one_abscon_trans authentic (n, c) =
    1.14 -          (if authentic then ParsePrintRule else ParseRule)
    1.15 +          (if authentic then Parse_Print_Rule else Parse_Rule)
    1.16              (cabs (con1 authentic n c, expvar n),
    1.17               capps (case_constant, map_index (when1 n) spec))
    1.18        fun abscon_trans authentic =
    1.19 @@ -479,7 +479,7 @@
    1.20            case_trans false :: case_trans true ::
    1.21            abscon_trans false @ abscon_trans true
    1.22      in
    1.23 -      val thy = Sign.add_trrules_i trans_rules thy
    1.24 +      val thy = Sign.add_trrules trans_rules thy
    1.25      end
    1.26  
    1.27      (* prove beta reduction rule for case combinator *)
     2.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 03 18:17:21 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 03 21:59:33 2011 +0200
     2.3 @@ -24,9 +24,9 @@
     2.4  fun trans_rules name2 name1 n mx =
     2.5    let
     2.6      val vnames = Name.invents Name.context "a" n
     2.7 -    val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1)
     2.8 +    val extra_parse_rule = Syntax.Parse_Rule (Constant name2, Constant name1)
     2.9    in
    2.10 -    [Syntax.ParsePrintRule
    2.11 +    [Syntax.Parse_Print_Rule
    2.12        (Syntax.mk_appl (Constant name2) (map Variable vnames),
    2.13          fold (fn a => fn t => Syntax.mk_appl (Constant @{const_syntax Rep_cfun}) [t, Variable a])
    2.14            vnames (Constant name1))] @
    2.15 @@ -80,7 +80,7 @@
    2.16    in
    2.17      thy
    2.18      |> Sign.add_consts_i (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
    2.19 -    |> Sign.add_trrules_i (maps #3 transformed_decls)
    2.20 +    |> Sign.add_trrules (maps #3 transformed_decls)
    2.21    end
    2.22  
    2.23  in
     3.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Apr 03 18:17:21 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Apr 03 21:59:33 2011 +0200
     3.3 @@ -516,17 +516,17 @@
     3.4            val ps = map (fn n => Variable ("p"^(string_of_int n))) ns;
     3.5            val vs = map (fn n => Variable ("v"^(string_of_int n))) ns;
     3.6          in
     3.7 -          [ParseRule (app_pat (capps (cname, xs)),
     3.8 +          [Parse_Rule (app_pat (capps (cname, xs)),
     3.9                        mk_appl pname (map app_pat xs)),
    3.10 -           ParseRule (app_var (capps (cname, xs)),
    3.11 +           Parse_Rule (app_var (capps (cname, xs)),
    3.12                        app_var (args_list xs)),
    3.13 -           PrintRule (capps (cname, ListPair.map (app "_match") (ps,vs)),
    3.14 +           Print_Rule (capps (cname, ListPair.map (app "_match") (ps,vs)),
    3.15                        app "_match" (mk_appl pname ps, args_list vs))]
    3.16          end;
    3.17        val trans_rules : Syntax.ast Syntax.trrule list =
    3.18            maps one_case_trans (pat_consts ~~ spec);
    3.19      in
    3.20 -      val thy = Sign.add_trrules_i trans_rules thy;
    3.21 +      val thy = Sign.add_trrules trans_rules thy;
    3.22      end;
    3.23  
    3.24      (* prove strictness and reduction rules of pattern combinators *)
     4.1 --- a/src/Pure/General/position.ML	Sun Apr 03 18:17:21 2011 +0200
     4.2 +++ b/src/Pure/General/position.ML	Sun Apr 03 21:59:33 2011 +0200
     4.3 @@ -34,6 +34,8 @@
     4.4    val reported_text: T -> Markup.T -> string -> string
     4.5    val report_text: T -> Markup.T -> string -> unit
     4.6    val report: T -> Markup.T -> unit
     4.7 +  type reports = (T * Markup.T) list
     4.8 +  val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
     4.9    val str_of: T -> string
    4.10    type range = T * T
    4.11    val no_range: range
    4.12 @@ -155,6 +157,13 @@
    4.13  fun report_text pos markup txt = Output.report (reported_text pos markup txt);
    4.14  fun report pos markup = report_text pos markup "";
    4.15  
    4.16 +type reports = (T * Markup.T) list;
    4.17 +
    4.18 +fun reports _ [] _ _ = ()
    4.19 +  | reports (r: reports Unsynchronized.ref) ps markup x =
    4.20 +      let val ms = markup x
    4.21 +      in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
    4.22 +
    4.23  
    4.24  (* str_of *)
    4.25  
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Apr 03 18:17:21 2011 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Apr 03 21:59:33 2011 +0200
     5.3 @@ -13,6 +13,8 @@
     5.4    val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     5.5    val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     5.6    val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
     5.7 +  val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     5.8 +  val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     5.9    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    5.10    val add_axioms: (Attrib.binding * string) list -> theory -> theory
    5.11    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    5.12 @@ -154,6 +156,22 @@
    5.13  end;
    5.14  
    5.15  
    5.16 +(* translation rules *)
    5.17 +
    5.18 +fun read_trrules thy raw_rules =
    5.19 +  let
    5.20 +    val ctxt = ProofContext.init_global thy;
    5.21 +    val type_ctxt = ProofContext.type_context ctxt;
    5.22 +    val syn = ProofContext.syn_of ctxt;
    5.23 +  in
    5.24 +    raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
    5.25 +      Syntax.read_rule_pattern ctxt type_ctxt syn (Sign.intern_type thy r, s)))
    5.26 +  end;
    5.27 +
    5.28 +fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
    5.29 +fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy;
    5.30 +
    5.31 +
    5.32  (* oracles *)
    5.33  
    5.34  fun oracle (name, pos) (body_txt, body_pos) =
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 03 18:17:21 2011 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 03 21:59:33 2011 +0200
     6.3 @@ -175,9 +175,9 @@
     6.4      -- Parse.string;
     6.5  
     6.6  fun trans_arrow toks =
     6.7 -  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
     6.8 -    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
     6.9 -    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
    6.10 +  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
    6.11 +    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
    6.12 +    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
    6.13  
    6.14  val trans_line =
    6.15    trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
    6.16 @@ -185,11 +185,11 @@
    6.17  
    6.18  val _ =
    6.19    Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
    6.20 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
    6.21 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
    6.22  
    6.23  val _ =
    6.24    Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
    6.25 -    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
    6.26 +    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
    6.27  
    6.28  
    6.29  (* axioms and definitions *)
     7.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 03 18:17:21 2011 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Apr 03 21:59:33 2011 +0200
     7.3 @@ -65,7 +65,9 @@
     7.4    val allow_dummies: Proof.context -> Proof.context
     7.5    val check_tvar: Proof.context -> indexname * sort -> indexname * sort
     7.6    val check_tfree: Proof.context -> string * sort -> string * sort
     7.7 -  val decode_term: Proof.context -> term -> (Position.T * Markup.T) list * term
     7.8 +  val type_context: Proof.context -> Syntax.type_context
     7.9 +  val term_context: Proof.context -> Syntax.term_context
    7.10 +  val decode_term: Proof.context -> Position.reports * term -> Position.reports * term
    7.11    val standard_infer_types: Proof.context -> term list -> term list
    7.12    val read_term_pattern: Proof.context -> string -> term
    7.13    val read_term_schematic: Proof.context -> string -> term
    7.14 @@ -665,12 +667,18 @@
    7.15  
    7.16  in
    7.17  
    7.18 +fun type_context ctxt : Syntax.type_context =
    7.19 + {get_class = read_class ctxt,
    7.20 +  get_type = #1 o dest_Type o read_type_name_proper ctxt false,
    7.21 +  markup_class = fn c => [Name_Space.markup_entry (Type.class_space (tsig_of ctxt)) c],
    7.22 +  markup_type = fn c => [Name_Space.markup_entry (Type.type_space (tsig_of ctxt)) c]};
    7.23 +
    7.24  fun term_context ctxt : Syntax.term_context =
    7.25   {get_sort = get_sort ctxt,
    7.26    get_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
    7.27      handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
    7.28    get_free = intern_skolem ctxt (Variable.def_type ctxt false),
    7.29 -  markup_const = fn x => [Name_Space.markup_entry (const_space ctxt) x],
    7.30 +  markup_const = fn c => [Name_Space.markup_entry (const_space ctxt) c],
    7.31    markup_free = fn x =>
    7.32      [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
    7.33      (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then [] else [Markup.hilite]),
    7.34 @@ -748,14 +756,16 @@
    7.35  fun parse_sort ctxt text =
    7.36    let
    7.37      val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    7.38 -    val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
    7.39 +    val S =
    7.40 +      Syntax.standard_parse_sort ctxt (type_context ctxt) (syn_of ctxt) (syms, pos)
    7.41        handle ERROR msg => parse_failed ctxt pos msg "sort";
    7.42    in Type.minimize_sort (tsig_of ctxt) S end;
    7.43  
    7.44  fun parse_typ ctxt text =
    7.45    let
    7.46      val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    7.47 -    val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
    7.48 +    val T =
    7.49 +      Syntax.standard_parse_typ ctxt (type_context ctxt) (syn_of ctxt) (get_sort ctxt) (syms, pos)
    7.50        handle ERROR msg => parse_failed ctxt pos msg "type";
    7.51    in T end;
    7.52  
    7.53 @@ -777,8 +787,9 @@
    7.54      fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
    7.55        handle ERROR msg => SOME msg;
    7.56      val t =
    7.57 -      Syntax.standard_parse_term check (term_context ctxt) ctxt (syn_of ctxt) root (syms, pos)
    7.58 -        handle ERROR msg => parse_failed ctxt pos msg kind;
    7.59 +      Syntax.standard_parse_term check ctxt (type_context ctxt) (term_context ctxt) (syn_of ctxt)
    7.60 +        root (syms, pos)
    7.61 +      handle ERROR msg => parse_failed ctxt pos msg kind;
    7.62    in t end;
    7.63  
    7.64  
    7.65 @@ -1079,13 +1090,6 @@
    7.66  
    7.67  (* authentic syntax *)
    7.68  
    7.69 -val _ = Context.>>
    7.70 -  (Context.map_theory
    7.71 -    (Sign.add_advanced_trfuns
    7.72 -      (Syntax.type_ast_trs
    7.73 -        {read_class = read_class,
    7.74 -          read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
    7.75 -
    7.76  local
    7.77  
    7.78  fun const_ast_tr intern ctxt [Syntax.Variable c] =
     8.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Apr 03 18:17:21 2011 +0200
     8.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Apr 03 21:59:33 2011 +0200
     8.3 @@ -70,7 +70,7 @@
     8.4         (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
     8.5    |> Sign.add_modesyntax_i ("latex", false)
     8.6        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
     8.7 -  |> Sign.add_trrules_i (map Syntax.ParsePrintRule
     8.8 +  |> Sign.add_trrules (map Syntax.Parse_Print_Rule
     8.9        [(Syntax.mk_appl (Constant "_Lam")
    8.10            [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    8.11          Syntax.mk_appl (Constant "_Lam")
     9.1 --- a/src/Pure/Syntax/syn_trans.ML	Sun Apr 03 18:17:21 2011 +0200
     9.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sun Apr 03 21:59:33 2011 +0200
     9.3 @@ -48,6 +48,7 @@
     9.4      (string * (term list -> term)) list *
     9.5      (string * (bool -> typ -> term list -> term)) list *
     9.6      (string * (Ast.ast list -> Ast.ast)) list
     9.7 +  type type_context
     9.8  end;
     9.9  
    9.10  signature SYN_TRANS =
    9.11 @@ -57,8 +58,9 @@
    9.12    val prop_tr': term -> term
    9.13    val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    9.14    val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    9.15 -  val parsetree_to_ast: Proof.context -> bool ->
    9.16 -    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    9.17 +  val parsetree_to_ast: Proof.context -> type_context -> bool ->
    9.18 +    (string -> (Proof.context -> Ast.ast list -> Ast.ast) option) ->
    9.19 +    Parser.parsetree -> Position.reports * Ast.ast
    9.20    val ast_to_term: Proof.context ->
    9.21      (string -> (Proof.context -> term list -> term) option) -> Ast.ast -> term
    9.22  end;
    9.23 @@ -549,21 +551,44 @@
    9.24  
    9.25  (** parsetree_to_ast **)
    9.26  
    9.27 -fun parsetree_to_ast ctxt constrain_pos trf =
    9.28 +type type_context =
    9.29 + {get_class: string -> string,
    9.30 +  get_type: string -> string,
    9.31 +  markup_class: string -> Markup.T list,
    9.32 +  markup_type: string -> Markup.T list};
    9.33 +
    9.34 +fun parsetree_to_ast ctxt (type_context: type_context) constrain_pos trf parsetree =
    9.35    let
    9.36 +    val {get_class, get_type, markup_class, markup_type} = type_context;
    9.37 +
    9.38 +    val reports = Unsynchronized.ref ([]: Position.reports);
    9.39 +    fun report pos = Position.reports reports [pos];
    9.40 +
    9.41      fun trans a args =
    9.42        (case trf a of
    9.43          NONE => Ast.mk_appl (Ast.Constant a) args
    9.44        | SOME f => f ctxt args);
    9.45  
    9.46 -    fun ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
    9.47 +    fun ast_of (Parser.Node ("_class_name", [Parser.Tip tok])) =
    9.48 +          let
    9.49 +            val c = get_class (Lexicon.str_of_token tok);
    9.50 +            val _ = report (Lexicon.pos_of_token tok) markup_class c;
    9.51 +          in Ast.Constant (Lexicon.mark_class c) end
    9.52 +      | ast_of (Parser.Node ("_type_name", [Parser.Tip tok])) =
    9.53 +          let
    9.54 +            val c = get_type (Lexicon.str_of_token tok);
    9.55 +            val _ = report (Lexicon.pos_of_token tok) markup_type c;
    9.56 +          in Ast.Constant (Lexicon.mark_type c) end
    9.57 +      | ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
    9.58            if constrain_pos then
    9.59              Ast.Appl [Ast.Constant "_constrain", ast_of pt,
    9.60                Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
    9.61            else ast_of pt
    9.62        | ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    9.63        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
    9.64 -  in ast_of end;
    9.65 +
    9.66 +    val ast = ast_of parsetree;
    9.67 +  in (! reports, ast) end;
    9.68  
    9.69  
    9.70  
    10.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 03 18:17:21 2011 +0200
    10.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Apr 03 21:59:33 2011 +0200
    10.3 @@ -116,17 +116,20 @@
    10.4    val ambiguity_level_raw: Config.raw
    10.5    val ambiguity_level: int Config.T
    10.6    val ambiguity_limit: int Config.T
    10.7 -  val standard_parse_term: (term -> string option) -> term_context ->
    10.8 -    Proof.context -> syntax -> string -> Symbol_Pos.T list * Position.T -> term
    10.9 -  val standard_parse_typ: Proof.context -> syntax ->
   10.10 +  val standard_parse_term: (term -> string option) ->
   10.11 +    Proof.context -> type_context -> term_context -> syntax ->
   10.12 +    string -> Symbol_Pos.T list * Position.T -> term
   10.13 +  val standard_parse_typ: Proof.context -> type_context -> syntax ->
   10.14      ((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
   10.15 -  val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
   10.16 +  val standard_parse_sort: Proof.context -> type_context -> syntax ->
   10.17 +    Symbol_Pos.T list * Position.T -> sort
   10.18    datatype 'a trrule =
   10.19 -    ParseRule of 'a * 'a |
   10.20 -    PrintRule of 'a * 'a |
   10.21 -    ParsePrintRule of 'a * 'a
   10.22 +    Parse_Rule of 'a * 'a |
   10.23 +    Print_Rule of 'a * 'a |
   10.24 +    Parse_Print_Rule of 'a * 'a
   10.25    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   10.26    val is_const: syntax -> string -> bool
   10.27 +  val read_rule_pattern: Proof.context -> type_context -> syntax -> string * string -> ast
   10.28    val standard_unparse_term: {structs: string list, fixes: string list} ->
   10.29      {extern_class: string -> xstring, extern_type: string -> xstring,
   10.30        extern_const: string -> xstring} -> Proof.context -> syntax -> bool -> term -> Pretty.T
   10.31 @@ -149,10 +152,8 @@
   10.32    val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   10.33    val update_const_gram: bool -> (string -> bool) ->
   10.34      mode -> (string * typ * mixfix) list -> syntax -> syntax
   10.35 -  val update_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
   10.36 -  val remove_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
   10.37 -  val update_trrules_i: ast trrule list -> syntax -> syntax
   10.38 -  val remove_trrules_i: ast trrule list -> syntax -> syntax
   10.39 +  val update_trrules: ast trrule list -> syntax -> syntax
   10.40 +  val remove_trrules: ast trrule list -> syntax -> syntax
   10.41  end;
   10.42  
   10.43  structure Syntax: SYNTAX =
   10.44 @@ -619,8 +620,8 @@
   10.45  val basic_nonterms =
   10.46    (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
   10.47      Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
   10.48 -    "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
   10.49 -    "index", "struct", "id_position", "longid_position"]);
   10.50 +    "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index",
   10.51 +    "struct", "id_position", "longid_position", "type_name", "class_name"]);
   10.52  
   10.53  
   10.54  
   10.55 @@ -711,7 +712,7 @@
   10.56  
   10.57  fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
   10.58  
   10.59 -fun read_asts ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   10.60 +fun read_asts ctxt type_ctxt (Syntax (tabs, _)) raw root (syms, pos) =
   10.61    let
   10.62      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
   10.63      val toks = Lexicon.tokenize lexicon raw syms;
   10.64 @@ -725,7 +726,8 @@
   10.65  
   10.66      val limit = Config.get ctxt ambiguity_limit;
   10.67      fun show_pt pt =
   10.68 -      Pretty.string_of (Ast.pretty_ast (Syn_Trans.parsetree_to_ast ctxt false (K NONE) pt));
   10.69 +      Pretty.string_of
   10.70 +        (Ast.pretty_ast (#2 (Syn_Trans.parsetree_to_ast ctxt type_ctxt false (K NONE) pt)));
   10.71      val _ =
   10.72        if len <= Config.get ctxt ambiguity_level then ()
   10.73        else if not (Config.get ctxt ambiguity_enabled) then error (ambiguity_msg pos)
   10.74 @@ -738,17 +740,18 @@
   10.75  
   10.76      val constrain_pos = not raw andalso Config.get ctxt positions;
   10.77    in
   10.78 -    some_results (Syn_Trans.parsetree_to_ast ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
   10.79 +    some_results
   10.80 +      (Syn_Trans.parsetree_to_ast ctxt type_ctxt constrain_pos (lookup_tr parse_ast_trtab)) pts
   10.81    end;
   10.82  
   10.83  
   10.84  (* read *)
   10.85  
   10.86 -fun read ctxt (syn as Syntax (tabs, _)) root inp =
   10.87 +fun read ctxt type_ctxt (syn as Syntax (tabs, _)) root inp =
   10.88    let val {parse_ruletab, parse_trtab, ...} = tabs in
   10.89 -    read_asts ctxt syn false root inp
   10.90 -    |> map (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab))
   10.91 -    |> some_results (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab))
   10.92 +    read_asts ctxt type_ctxt syn false root inp
   10.93 +    |> map (apsnd (Ast.normalize ctxt (Symtab.lookup_list parse_ruletab)))
   10.94 +    |> some_results (apsnd (Syn_Trans.ast_to_term ctxt (lookup_tr parse_trtab)))
   10.95    end;
   10.96  
   10.97  
   10.98 @@ -790,51 +793,60 @@
   10.99              map (show_term o snd) (take limit results)))
  10.100        end;
  10.101  
  10.102 -fun standard_parse_term check term_ctxt ctxt syn root (syms, pos) =
  10.103 -  read ctxt syn root (syms, pos)
  10.104 +fun standard_parse_term check ctxt type_ctxt term_ctxt syn root (syms, pos) =
  10.105 +  read ctxt type_ctxt syn root (syms, pos)
  10.106    |> map (Type_Ext.decode_term term_ctxt)
  10.107    |> disambig ctxt check;
  10.108  
  10.109  
  10.110  (* read types *)
  10.111  
  10.112 -fun standard_parse_typ ctxt syn get_sort (syms, pos) =
  10.113 -  (case read ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
  10.114 -    [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
  10.115 +fun standard_parse_typ ctxt type_ctxt syn get_sort (syms, pos) =
  10.116 +  (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
  10.117 +    [res] =>
  10.118 +      let val t = report_result ctxt res
  10.119 +      in Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t end
  10.120    | _ => error (ambiguity_msg pos));
  10.121  
  10.122  
  10.123  (* read sorts *)
  10.124  
  10.125 -fun standard_parse_sort ctxt syn (syms, pos) =
  10.126 -  (case read ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
  10.127 -    [t] => Type_Ext.sort_of_term t
  10.128 +fun standard_parse_sort ctxt type_ctxt syn (syms, pos) =
  10.129 +  (case read ctxt type_ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
  10.130 +    [res] =>
  10.131 +      let val t = report_result ctxt res
  10.132 +      in Type_Ext.sort_of_term t end
  10.133    | _ => error (ambiguity_msg pos));
  10.134  
  10.135  
  10.136  
  10.137  (** prepare translation rules **)
  10.138  
  10.139 +(* rules *)
  10.140 +
  10.141  datatype 'a trrule =
  10.142 -  ParseRule of 'a * 'a |
  10.143 -  PrintRule of 'a * 'a |
  10.144 -  ParsePrintRule of 'a * 'a;
  10.145 +  Parse_Rule of 'a * 'a |
  10.146 +  Print_Rule of 'a * 'a |
  10.147 +  Parse_Print_Rule of 'a * 'a;
  10.148  
  10.149 -fun map_trrule f (ParseRule (x, y)) = ParseRule (f x, f y)
  10.150 -  | map_trrule f (PrintRule (x, y)) = PrintRule (f x, f y)
  10.151 -  | map_trrule f (ParsePrintRule (x, y)) = ParsePrintRule (f x, f y);
  10.152 +fun map_trrule f (Parse_Rule (x, y)) = Parse_Rule (f x, f y)
  10.153 +  | map_trrule f (Print_Rule (x, y)) = Print_Rule (f x, f y)
  10.154 +  | map_trrule f (Parse_Print_Rule (x, y)) = Parse_Print_Rule (f x, f y);
  10.155  
  10.156 -fun parse_rule (ParseRule pats) = SOME pats
  10.157 -  | parse_rule (PrintRule _) = NONE
  10.158 -  | parse_rule (ParsePrintRule pats) = SOME pats;
  10.159 +fun parse_rule (Parse_Rule pats) = SOME pats
  10.160 +  | parse_rule (Print_Rule _) = NONE
  10.161 +  | parse_rule (Parse_Print_Rule pats) = SOME pats;
  10.162  
  10.163 -fun print_rule (ParseRule _) = NONE
  10.164 -  | print_rule (PrintRule pats) = SOME (swap pats)
  10.165 -  | print_rule (ParsePrintRule pats) = SOME (swap pats);
  10.166 +fun print_rule (Parse_Rule _) = NONE
  10.167 +  | print_rule (Print_Rule pats) = SOME (swap pats)
  10.168 +  | print_rule (Parse_Print_Rule pats) = SOME (swap pats);
  10.169  
  10.170  
  10.171  fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
  10.172  
  10.173 +
  10.174 +(* check_rules *)
  10.175 +
  10.176  local
  10.177  
  10.178  fun check_rule rule =
  10.179 @@ -844,7 +856,18 @@
  10.180          Pretty.string_of (Ast.pretty_rule rule))
  10.181    | NONE => rule);
  10.182  
  10.183 -fun read_pattern ctxt syn (root, str) =
  10.184 +in
  10.185 +
  10.186 +fun check_rules rules =
  10.187 + (map check_rule (map_filter parse_rule rules),
  10.188 +  map check_rule (map_filter print_rule rules));
  10.189 +
  10.190 +end;
  10.191 +
  10.192 +
  10.193 +(* read_rule_pattern *)
  10.194 +
  10.195 +fun read_rule_pattern ctxt type_ctxt syn (root, str) =
  10.196    let
  10.197      fun constify (ast as Ast.Constant _) = ast
  10.198        | constify (ast as Ast.Variable x) =
  10.199 @@ -854,25 +877,13 @@
  10.200  
  10.201      val (syms, pos) = read_token str;
  10.202    in
  10.203 -    (case read_asts ctxt syn true root (syms, pos) of
  10.204 -      [ast] => constify ast
  10.205 +    (case read_asts ctxt type_ctxt syn true root (syms, pos) of
  10.206 +      [res] =>
  10.207 +        let val ast = report_result ctxt res
  10.208 +        in constify ast end
  10.209      | _ => error (ambiguity_msg pos))
  10.210    end;
  10.211  
  10.212 -fun prep_rules rd_pat raw_rules =
  10.213 -  let val rules = map (map_trrule rd_pat) raw_rules in
  10.214 -    (map check_rule (map_filter parse_rule rules),
  10.215 -      map check_rule (map_filter print_rule rules))
  10.216 -  end
  10.217 -
  10.218 -in
  10.219 -
  10.220 -val cert_rules = prep_rules I;
  10.221 -
  10.222 -fun read_rules ctxt syn = prep_rules (read_pattern ctxt syn);
  10.223 -
  10.224 -end;
  10.225 -
  10.226  
  10.227  
  10.228  (** unparse terms, typs, sorts **)
  10.229 @@ -920,14 +931,8 @@
  10.230  fun update_const_gram add is_logtype prmode decls =
  10.231    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
  10.232  
  10.233 -fun update_trrules ctxt syn =
  10.234 -  ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt syn;
  10.235 -
  10.236 -fun remove_trrules ctxt syn =
  10.237 -  remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt syn;
  10.238 -
  10.239 -val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
  10.240 -val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
  10.241 +val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules;
  10.242 +val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules;
  10.243  
  10.244  
  10.245  (*export parts of internal Syntax structures*)
    11.1 --- a/src/Pure/Syntax/type_ext.ML	Sun Apr 03 18:17:21 2011 +0200
    11.2 +++ b/src/Pure/Syntax/type_ext.ML	Sun Apr 03 21:59:33 2011 +0200
    11.3 @@ -13,14 +13,10 @@
    11.4    val strip_positions: term -> term
    11.5    val strip_positions_ast: Ast.ast -> Ast.ast
    11.6    type term_context
    11.7 -  val decode_term: term_context -> term -> (Position.T * Markup.T) list * term
    11.8 +  val decode_term: term_context -> Position.reports * term -> Position.reports * term
    11.9    val term_of_typ: bool -> typ -> term
   11.10    val no_brackets: unit -> bool
   11.11    val no_type_brackets: unit -> bool
   11.12 -  val type_ast_trs:
   11.13 -   {read_class: Proof.context -> string -> string,
   11.14 -    read_type: Proof.context -> string -> string} ->
   11.15 -    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
   11.16  end;
   11.17  
   11.18  signature TYPE_EXT =
   11.19 @@ -140,16 +136,13 @@
   11.20    markup_free: string -> Markup.T list,
   11.21    markup_var: indexname -> Markup.T list};
   11.22  
   11.23 -fun decode_term (term_context: term_context) tm =
   11.24 +fun decode_term (term_context: term_context) (reports0: Position.reports, tm) =
   11.25    let
   11.26      val {get_sort, get_const, get_free, markup_const, markup_free, markup_var} = term_context;
   11.27      val decodeT = typ_of_term (get_sort (term_sorts tm));
   11.28  
   11.29 -    val reports = Unsynchronized.ref ([]: (Position.T * Markup.T) list);
   11.30 -    fun report [] _ _ = ()
   11.31 -      | report ps markup x =
   11.32 -          let val ms = markup x
   11.33 -          in Unsynchronized.change reports (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
   11.34 +    val reports = Unsynchronized.ref reports0;
   11.35 +    fun report ps = Position.reports reports ps;
   11.36  
   11.37      fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
   11.38            (case decode_position typ of
   11.39 @@ -252,30 +245,14 @@
   11.40  
   11.41  (* parse ast translations *)
   11.42  
   11.43 -val class_ast = Ast.Constant o Lexicon.mark_class;
   11.44 -val type_ast = Ast.Constant o Lexicon.mark_type;
   11.45 -
   11.46 -fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
   11.47 -  | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
   11.48 -
   11.49 -fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
   11.50 -      Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
   11.51 -  | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
   11.52 +fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
   11.53 +  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
   11.54  
   11.55 -fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
   11.56 -  | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
   11.57 -
   11.58 -fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
   11.59 -      Ast.Appl [type_ast (read_type c), ty]
   11.60 -  | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
   11.61 +fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
   11.62 +  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
   11.63  
   11.64 -fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
   11.65 -      Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
   11.66 -  | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
   11.67 -
   11.68 -fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   11.69 -      Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   11.70 -  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
   11.71 +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   11.72 +  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
   11.73  
   11.74  
   11.75  (* print ast translations *)
   11.76 @@ -296,32 +273,35 @@
   11.77  
   11.78  (* type_ext *)
   11.79  
   11.80 -val sortT = Type ("sort", []);
   11.81 -val classesT = Type ("classes", []);
   11.82 -val typesT = Type ("types", []);
   11.83 +fun typ c = Type (c, []);
   11.84 +
   11.85 +val class_nameT = typ "class_name";
   11.86 +val type_nameT = typ "type_name";
   11.87 +
   11.88 +val sortT = typ "sort";
   11.89 +val classesT = typ "classes";
   11.90 +val typesT = typ "types";
   11.91  
   11.92  local open Lexicon Syn_Ext in
   11.93  
   11.94  val type_ext = syn_ext' false (K false)
   11.95    [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   11.96     Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   11.97 -   Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
   11.98 -   Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
   11.99 +   Mfix ("_",           type_nameT --> typeT,          "", [], max_pri),
  11.100 +   Mfix ("_",           idT --> type_nameT,            "_type_name", [], max_pri),
  11.101 +   Mfix ("_",           longidT --> type_nameT,        "_type_name", [], max_pri),
  11.102     Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
  11.103     Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
  11.104     Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
  11.105 -   Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
  11.106 -   Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
  11.107 +   Mfix ("_",           class_nameT --> sortT,         "", [], max_pri),
  11.108 +   Mfix ("_",           idT --> class_nameT,           "_class_name", [], max_pri),
  11.109 +   Mfix ("_",           longidT --> class_nameT,       "_class_name", [], max_pri),
  11.110     Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
  11.111     Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
  11.112 -   Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
  11.113 -   Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
  11.114 -   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
  11.115 -   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
  11.116 -   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
  11.117 -   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
  11.118 -   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
  11.119 -   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
  11.120 +   Mfix ("_",           class_nameT --> classesT,      "", [], max_pri),
  11.121 +   Mfix ("_,_",         [class_nameT, classesT] ---> classesT, "_classes", [], max_pri),
  11.122 +   Mfix ("_ _",         [typeT, type_nameT] ---> typeT, "_tapp", [max_pri, 0], max_pri),
  11.123 +   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, type_nameT] ---> typeT, "_tappl", [], max_pri),
  11.124     Mfix ("_",           typeT --> typesT,              "", [], max_pri),
  11.125     Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
  11.126     Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
  11.127 @@ -329,18 +309,12 @@
  11.128     Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
  11.129     Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
  11.130    ["_type_prop"]
  11.131 -  ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
  11.132 +  (map Syn_Ext.mk_trfun
  11.133 +    [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
  11.134 +   [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
  11.135    []
  11.136    ([], []);
  11.137  
  11.138 -fun type_ast_trs {read_class, read_type} =
  11.139 - [("_class_name", class_name_tr o read_class),
  11.140 -  ("_classes", classes_tr o read_class),
  11.141 -  ("_type_name", type_name_tr o read_type),
  11.142 -  ("_tapp", tapp_ast_tr o read_type),
  11.143 -  ("_tappl", tappl_ast_tr o read_type),
  11.144 -  ("_bracket", K bracket_ast_tr)];
  11.145 -
  11.146  end;
  11.147  
  11.148  end;
    12.1 --- a/src/Pure/sign.ML	Sun Apr 03 18:17:21 2011 +0200
    12.2 +++ b/src/Pure/sign.ML	Sun Apr 03 21:59:33 2011 +0200
    12.3 @@ -108,10 +108,8 @@
    12.4      (string * string * (Proof.context -> string -> Pretty.T)) list -> theory -> theory
    12.5    val add_mode_tokentrfuns: string -> (string * (Proof.context -> string -> Pretty.T)) list
    12.6      -> theory -> theory
    12.7 -  val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    12.8 -  val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
    12.9 -  val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   12.10 -  val del_trrules_i: ast Syntax.trrule list -> theory -> theory
   12.11 +  val add_trrules: ast Syntax.trrule list -> theory -> theory
   12.12 +  val del_trrules: ast Syntax.trrule list -> theory -> theory
   12.13    val new_group: theory -> theory
   12.14    val reset_group: theory -> theory
   12.15    val add_path: string -> theory -> theory
   12.16 @@ -497,14 +495,8 @@
   12.17  
   12.18  (* translation rules *)
   12.19  
   12.20 -fun gen_trrules f args thy = thy |> map_syn (fn syn =>
   12.21 -  let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
   12.22 -  in f (ProofContext.init_global thy) syn rules syn end);
   12.23 -
   12.24 -val add_trrules = gen_trrules Syntax.update_trrules;
   12.25 -val del_trrules = gen_trrules Syntax.remove_trrules;
   12.26 -val add_trrules_i = map_syn o Syntax.update_trrules_i;
   12.27 -val del_trrules_i = map_syn o Syntax.remove_trrules_i;
   12.28 +val add_trrules = map_syn o Syntax.update_trrules;
   12.29 +val del_trrules = map_syn o Syntax.remove_trrules;
   12.30  
   12.31  
   12.32  (* naming *)