discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
authorwenzelm
Fri Apr 08 15:02:11 2011 +0200 (2011-04-08)
changeset 422882074b31650e6
parent 42287 d98eb048a2e4
child 42289 dafae095d733
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
clarified Syntax.root;
doc-src/Codegen/Thy/Setup.thy
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Library/OptionalSugar.thy
src/Pure/IsaMakefile
src/Pure/Isar/auto_bind.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ROOT.ML
src/Pure/Syntax/local_syntax.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/doc-src/Codegen/Thy/Setup.thy	Fri Apr 08 14:20:57 2011 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Fri Apr 08 15:02:11 2011 +0200
     1.3 @@ -10,8 +10,8 @@
     1.4  setup {*
     1.5  let
     1.6    val typ = Simple_Syntax.read_typ;
     1.7 -  val typeT = Syntax.typeT;
     1.8 -  val spropT = Syntax.spropT;
     1.9 +  val typeT = Syntax_Ext.typeT;
    1.10 +  val spropT = Syntax_Ext.spropT;
    1.11  in
    1.12    Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    1.13      ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
     2.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Apr 08 14:20:57 2011 +0200
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Apr 08 15:02:11 2011 +0200
     2.3 @@ -51,7 +51,7 @@
     2.4  
     2.5  fun mk_syntax name i =
     2.6    let
     2.7 -    val syn = Syntax.escape name
     2.8 +    val syn = Syntax_Ext.escape name
     2.9      val args = space_implode ",/ " (replicate i "_")
    2.10    in
    2.11      if i = 0 then Mixfix (syn, [], 1000)
     3.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Fri Apr 08 14:20:57 2011 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Apr 08 15:02:11 2011 +0200
     3.3 @@ -11,8 +11,8 @@
     3.4  setup {*
     3.5  let
     3.6    val typ = Simple_Syntax.read_typ;
     3.7 -  val typeT = Syntax.typeT;
     3.8 -  val spropT = Syntax.spropT;
     3.9 +  val typeT = Syntax_Ext.typeT;
    3.10 +  val spropT = Syntax_Ext.spropT;
    3.11  in
    3.12    Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    3.13      ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
     4.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Apr 08 14:20:57 2011 +0200
     4.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Apr 08 15:02:11 2011 +0200
     4.3 @@ -182,7 +182,7 @@
     4.4  
     4.5  fun mk_syn thy c =
     4.6    if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     4.7 -  else Delimfix (Syntax.escape c)
     4.8 +  else Delimfix (Syntax_Ext.escape c)
     4.9  
    4.10  fun quotename c =
    4.11    if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
     5.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 14:20:57 2011 +0200
     5.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 15:02:11 2011 +0200
     5.3 @@ -51,8 +51,8 @@
     5.4  setup {*
     5.5  let
     5.6    val typ = Simple_Syntax.read_typ;
     5.7 -  val typeT = Syntax.typeT;
     5.8 -  val spropT = Syntax.spropT;
     5.9 +  val typeT = Syntax_Ext.typeT;
    5.10 +  val spropT = Syntax_Ext.spropT;
    5.11  in
    5.12    Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    5.13      ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
     6.1 --- a/src/Pure/IsaMakefile	Fri Apr 08 14:20:57 2011 +0200
     6.2 +++ b/src/Pure/IsaMakefile	Fri Apr 08 15:02:11 2011 +0200
     6.3 @@ -184,8 +184,8 @@
     6.4    Syntax/parser.ML					\
     6.5    Syntax/printer.ML					\
     6.6    Syntax/simple_syntax.ML				\
     6.7 -  Syntax/syn_ext.ML					\
     6.8    Syntax/syntax.ML					\
     6.9 +  Syntax/syntax_ext.ML					\
    6.10    Syntax/syntax_phases.ML				\
    6.11    Syntax/syntax_trans.ML				\
    6.12    Syntax/term_position.ML				\
     7.1 --- a/src/Pure/Isar/auto_bind.ML	Fri Apr 08 14:20:57 2011 +0200
     7.2 +++ b/src/Pure/Isar/auto_bind.ML	Fri Apr 08 15:02:11 2011 +0200
     7.3 @@ -45,8 +45,8 @@
     7.4  fun facts _ [] = []
     7.5    | facts thy props =
     7.6        let val prop = List.last props
     7.7 -      in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
     7.8 +      in [(Syntax_Ext.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
     7.9  
    7.10 -val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
    7.11 +val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
    7.12  
    7.13  end;
     8.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Fri Apr 08 14:20:57 2011 +0200
     8.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Fri Apr 08 15:02:11 2011 +0200
     8.3 @@ -23,8 +23,6 @@
     8.4  
     8.5  (** ML system and platform related **)
     8.6  
     8.7 -val forget_structure = PolyML.Compiler.forgetStructure;
     8.8 -
     8.9  val _ = PolyML.Compiler.forgetValue "isSome";
    8.10  val _ = PolyML.Compiler.forgetValue "getOpt";
    8.11  val _ = PolyML.Compiler.forgetValue "valOf";
     9.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Apr 08 14:20:57 2011 +0200
     9.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Fri Apr 08 15:02:11 2011 +0200
     9.3 @@ -103,8 +103,6 @@
     9.4      val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
     9.5    in use_text context (1, name) verbose txt end;
     9.6  
     9.7 -fun forget_structure _ = ();
     9.8 -
     9.9  
    9.10  (* toplevel pretty printing *)
    9.11  
    10.1 --- a/src/Pure/ROOT.ML	Fri Apr 08 14:20:57 2011 +0200
    10.2 +++ b/src/Pure/ROOT.ML	Fri Apr 08 15:02:11 2011 +0200
    10.3 @@ -122,7 +122,7 @@
    10.4  use "Syntax/lexicon.ML";
    10.5  use "Syntax/simple_syntax.ML";
    10.6  use "Syntax/ast.ML";
    10.7 -use "Syntax/syn_ext.ML";
    10.8 +use "Syntax/syntax_ext.ML";
    10.9  use "Syntax/parser.ML";
   10.10  use "Syntax/syntax_trans.ML";
   10.11  use "Syntax/mixfix.ML";
    11.1 --- a/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 14:20:57 2011 +0200
    11.2 +++ b/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 15:02:11 2011 +0200
    11.3 @@ -61,8 +61,8 @@
    11.4      val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
    11.5      val local_syntax = thy_syntax
    11.6        |> Syntax.update_trfuns
    11.7 -          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    11.8 -           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    11.9 +          (map Syntax_Ext.mk_trfun atrs, map Syntax_Ext.mk_trfun trs,
   11.10 +           map Syntax_Ext.mk_trfun trs', map Syntax_Ext.mk_trfun atrs')
   11.11        |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   11.12    in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;
   11.13  
    12.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:20:57 2011 +0200
    12.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 15:02:11 2011 +0200
    12.3 @@ -25,8 +25,8 @@
    12.4    val mixfixT: mixfix -> typ
    12.5    val make_type: int -> typ
    12.6    val binder_name: string -> string
    12.7 -  val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
    12.8 -  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
    12.9 +  val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
   12.10 +  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
   12.11  end;
   12.12  
   12.13  structure Mixfix: MIXFIX =
   12.14 @@ -74,11 +74,11 @@
   12.15  (* syntax specifications *)
   12.16  
   12.17  fun mixfix_args NoSyn = 0
   12.18 -  | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
   12.19 -  | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
   12.20 -  | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
   12.21 -  | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
   12.22 -  | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
   12.23 +  | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy
   12.24 +  | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy
   12.25 +  | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy
   12.26 +  | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy
   12.27 +  | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy
   12.28    | mixfix_args (Binder _) = 1
   12.29    | mixfix_args Structure = 0;
   12.30  
   12.31 @@ -88,29 +88,29 @@
   12.32  
   12.33  (* syn_ext_types *)
   12.34  
   12.35 -fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
   12.36 +fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
   12.37  
   12.38  fun syn_ext_types type_decls =
   12.39    let
   12.40 -    fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
   12.41 +    fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
   12.42  
   12.43      fun mfix_of (_, _, NoSyn) = NONE
   12.44 -      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
   12.45 -      | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
   12.46 +      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
   12.47 +      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
   12.48        | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
   12.49        | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
   12.50        | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
   12.51        | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);
   12.52  
   12.53 -    fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
   12.54 -          if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
   12.55 -          else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
   12.56 +    fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) =
   12.57 +          if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
   12.58 +          else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
   12.59        | check_args _ NONE = ();
   12.60  
   12.61      val mfix = map mfix_of type_decls;
   12.62      val _ = map2 check_args type_decls mfix;
   12.63      val xconsts = map #1 type_decls;
   12.64 -  in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
   12.65 +  in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
   12.66  
   12.67  
   12.68  (* syn_ext_consts *)
   12.69 @@ -121,21 +121,21 @@
   12.70  fun syn_ext_consts is_logtype const_decls =
   12.71    let
   12.72      fun mk_infix sy ty c p1 p2 p3 =
   12.73 -      [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
   12.74 -       Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
   12.75 +      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
   12.76 +       Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
   12.77  
   12.78      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
   12.79            [Type ("idts", []), ty2] ---> ty3
   12.80        | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
   12.81  
   12.82      fun mfix_of (_, _, NoSyn) = []
   12.83 -      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
   12.84 -      | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
   12.85 +      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
   12.86 +      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
   12.87        | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
   12.88        | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
   12.89        | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
   12.90        | mfix_of (c, ty, Binder (sy, p, q)) =
   12.91 -          [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
   12.92 +          [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
   12.93        | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);
   12.94  
   12.95      fun binder (c, _, Binder _) = SOME (binder_name c, c)
   12.96 @@ -145,12 +145,12 @@
   12.97      val xconsts = map #1 const_decls;
   12.98      val binders = map_filter binder const_decls;
   12.99      val binder_trs = binders
  12.100 -      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
  12.101 +      |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
  12.102      val binder_trs' = binders
  12.103 -      |> map (Syn_Ext.stamp_trfun binder_stamp o
  12.104 +      |> map (Syntax_Ext.stamp_trfun binder_stamp o
  12.105            apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
  12.106    in
  12.107 -    Syn_Ext.syn_ext' true is_logtype
  12.108 +    Syntax_Ext.syn_ext' true is_logtype
  12.109        mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
  12.110    end;
  12.111  
    13.1 --- a/src/Pure/Syntax/parser.ML	Fri Apr 08 14:20:57 2011 +0200
    13.2 +++ b/src/Pure/Syntax/parser.ML	Fri Apr 08 15:02:11 2011 +0200
    13.3 @@ -8,7 +8,7 @@
    13.4  sig
    13.5    type gram
    13.6    val empty_gram: gram
    13.7 -  val extend_gram: Syn_Ext.xprod list -> gram -> gram
    13.8 +  val extend_gram: Syntax_Ext.xprod list -> gram -> gram
    13.9    val merge_gram: gram * gram -> gram
   13.10    val pretty_gram: gram -> Pretty.T list
   13.11    datatype parsetree =
   13.12 @@ -468,10 +468,10 @@
   13.13            delimiters and predefined terms are stored as terminals,
   13.14            nonterminals are converted to integer tags*)
   13.15          fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
   13.16 -          | symb_of (Syn_Ext.Delim s :: ss) nt_count tags result =
   13.17 +          | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result =
   13.18                symb_of ss nt_count tags
   13.19                  (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
   13.20 -          | symb_of (Syn_Ext.Argument (s, p) :: ss) nt_count tags result =
   13.21 +          | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
   13.22                let
   13.23                  val (nt_count', tags', new_symb) =
   13.24                    (case Lexicon.predef_term s of
   13.25 @@ -485,7 +485,7 @@
   13.26          (*Convert list of productions by invoking symb_of for each of them*)
   13.27          fun prod_of [] nt_count prod_count tags result =
   13.28                (nt_count, prod_count, tags, result)
   13.29 -          | prod_of (Syn_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
   13.30 +          | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
   13.31                  nt_count prod_count tags result =
   13.32                let
   13.33                  val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;
    14.1 --- a/src/Pure/Syntax/printer.ML	Fri Apr 08 14:20:57 2011 +0200
    14.2 +++ b/src/Pure/Syntax/printer.ML	Fri Apr 08 15:02:11 2011 +0200
    14.3 @@ -30,8 +30,8 @@
    14.4    include PRINTER0
    14.5    type prtabs
    14.6    val empty_prtabs: prtabs
    14.7 -  val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
    14.8 -  val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
    14.9 +  val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   14.10 +  val remove_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
   14.11    val merge_prtabs: prtabs -> prtabs -> prtabs
   14.12    val pretty_term_ast: bool -> Proof.context -> prtabs ->
   14.13      (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
   14.14 @@ -93,29 +93,29 @@
   14.15  
   14.16  (* xprod_to_fmt *)
   14.17  
   14.18 -fun xprod_to_fmt (Syn_Ext.XProd (_, _, "", _)) = NONE
   14.19 -  | xprod_to_fmt (Syn_Ext.XProd (_, xsymbs, const, pri)) =
   14.20 +fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
   14.21 +  | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
   14.22        let
   14.23          fun arg (s, p) =
   14.24            (if s = "type" then TypArg else Arg)
   14.25 -          (if Lexicon.is_terminal s then Syn_Ext.max_pri else p);
   14.26 +          (if Lexicon.is_terminal s then Syntax_Ext.max_pri else p);
   14.27  
   14.28 -        fun xsyms_to_syms (Syn_Ext.Delim s :: xsyms) =
   14.29 +        fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
   14.30                apfst (cons (String s)) (xsyms_to_syms xsyms)
   14.31 -          | xsyms_to_syms (Syn_Ext.Argument s_p :: xsyms) =
   14.32 +          | xsyms_to_syms (Syntax_Ext.Argument s_p :: xsyms) =
   14.33                apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
   14.34 -          | xsyms_to_syms (Syn_Ext.Space s :: xsyms) =
   14.35 +          | xsyms_to_syms (Syntax_Ext.Space s :: xsyms) =
   14.36                apfst (cons (Space s)) (xsyms_to_syms xsyms)
   14.37 -          | xsyms_to_syms (Syn_Ext.Bg i :: xsyms) =
   14.38 +          | xsyms_to_syms (Syntax_Ext.Bg i :: xsyms) =
   14.39                let
   14.40                  val (bsyms, xsyms') = xsyms_to_syms xsyms;
   14.41                  val (syms, xsyms'') = xsyms_to_syms xsyms';
   14.42                in
   14.43                  (Block (i, bsyms) :: syms, xsyms'')
   14.44                end
   14.45 -          | xsyms_to_syms (Syn_Ext.Brk i :: xsyms) =
   14.46 +          | xsyms_to_syms (Syntax_Ext.Brk i :: xsyms) =
   14.47                apfst (cons (Break i)) (xsyms_to_syms xsyms)
   14.48 -          | xsyms_to_syms (Syn_Ext.En :: xsyms) = ([], xsyms)
   14.49 +          | xsyms_to_syms (Syntax_Ext.En :: xsyms) = ([], xsyms)
   14.50            | xsyms_to_syms [] = ([], []);
   14.51  
   14.52          fun nargs (Arg _ :: syms) = nargs syms + 1
   14.53 @@ -145,7 +145,7 @@
   14.54  fun remove_prtabs mode xprods prtabs =
   14.55    let
   14.56      val tab = mode_tab prtabs mode;
   14.57 -    val fmts = map_filter (fn xprod as Syn_Ext.XProd (_, _, c, _) =>
   14.58 +    val fmts = map_filter (fn xprod as Syntax_Ext.XProd (_, _, c, _) =>
   14.59        if null (Symtab.lookup_list tab c) then NONE
   14.60        else xprod_to_fmt xprod) xprods;
   14.61      val tab' = fold (Symtab.remove_list (op =)) fmts tab;
   14.62 @@ -210,10 +210,12 @@
   14.63              val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
   14.64            in (T :: Ts, args') end
   14.65  
   14.66 -    and parT m (pr, args, p, p': int) = #1 (synT m
   14.67 -          (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
   14.68 -            then [Block (1, Space "(" :: pr @ [Space ")"])]
   14.69 -            else pr, args))
   14.70 +    and parT m (pr, args, p, p': int) =
   14.71 +      #1 (synT m
   14.72 +          (if p > p' orelse
   14.73 +            (show_brackets andalso p' <> Syntax_Ext.max_pri andalso not (is_chain pr))
   14.74 +           then [Block (1, Space "(" :: pr @ [Space ")"])]
   14.75 +           else pr, args))
   14.76  
   14.77      and atomT a = Pretty.marks_str (markup_extern a)
   14.78  
    15.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Apr 08 14:20:57 2011 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,389 +0,0 @@
    15.4 -(*  Title:      Pure/Syntax/syn_ext.ML
    15.5 -    Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
    15.6 -
    15.7 -Syntax extension (internal interface).
    15.8 -*)
    15.9 -
   15.10 -signature SYN_EXT0 =
   15.11 -sig
   15.12 -  val dddot_indexname: indexname
   15.13 -  val typeT: typ
   15.14 -  val spropT: typ
   15.15 -  val default_root: string Config.T
   15.16 -  val max_pri: int
   15.17 -  val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   15.18 -  val mk_trfun: string * 'a -> string * ('a * stamp)
   15.19 -  val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
   15.20 -  val escape: string -> string
   15.21 -  val token_markers: string list
   15.22 -end;
   15.23 -
   15.24 -signature SYN_EXT =
   15.25 -sig
   15.26 -  include SYN_EXT0
   15.27 -  val logic: string
   15.28 -  val args: string
   15.29 -  val cargs: string
   15.30 -  val any: string
   15.31 -  val sprop: string
   15.32 -  datatype mfix = Mfix of string * typ * string * int list * int
   15.33 -  val err_in_mfix: string -> mfix -> 'a
   15.34 -  val typ_to_nonterm: typ -> string
   15.35 -  datatype xsymb =
   15.36 -    Delim of string |
   15.37 -    Argument of string * int |
   15.38 -    Space of string |
   15.39 -    Bg of int | Brk of int | En
   15.40 -  datatype xprod = XProd of string * xsymb list * string * int
   15.41 -  val chain_pri: int
   15.42 -  val delims_of: xprod list -> string list list
   15.43 -  datatype syn_ext =
   15.44 -    Syn_Ext of {
   15.45 -      xprods: xprod list,
   15.46 -      consts: string list,
   15.47 -      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
   15.48 -      parse_rules: (Ast.ast * Ast.ast) list,
   15.49 -      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
   15.50 -      print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
   15.51 -      print_rules: (Ast.ast * Ast.ast) list,
   15.52 -      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
   15.53 -  val mfix_delims: string -> string list
   15.54 -  val mfix_args: string -> int
   15.55 -  val syn_ext': bool -> (string -> bool) -> mfix list ->
   15.56 -    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   15.57 -    (string * ((Proof.context -> term list -> term) * stamp)) list *
   15.58 -    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   15.59 -    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
   15.60 -    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   15.61 -  val syn_ext: mfix list -> string list ->
   15.62 -    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   15.63 -    (string * ((Proof.context -> term list -> term) * stamp)) list *
   15.64 -    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   15.65 -    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
   15.66 -    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   15.67 -  val syn_ext_const_names: string list -> syn_ext
   15.68 -  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   15.69 -  val syn_ext_trfuns:
   15.70 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
   15.71 -    (string * ((term list -> term) * stamp)) list *
   15.72 -    (string * ((typ -> term list -> term) * stamp)) list *
   15.73 -    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   15.74 -  val syn_ext_advanced_trfuns:
   15.75 -    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   15.76 -    (string * ((Proof.context -> term list -> term) * stamp)) list *
   15.77 -    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   15.78 -    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   15.79 -  val pure_ext: syn_ext
   15.80 -end;
   15.81 -
   15.82 -structure Syn_Ext: SYN_EXT =
   15.83 -struct
   15.84 -
   15.85 -
   15.86 -(** misc definitions **)
   15.87 -
   15.88 -val dddot_indexname = ("dddot", 0);
   15.89 -
   15.90 -
   15.91 -(* syntactic categories *)
   15.92 -
   15.93 -val logic = "logic";
   15.94 -val logicT = Type (logic, []);
   15.95 -
   15.96 -val args = "args";
   15.97 -val cargs = "cargs";
   15.98 -
   15.99 -val typeT = Type ("type", []);
  15.100 -
  15.101 -val sprop = "#prop";
  15.102 -val spropT = Type (sprop, []);
  15.103 -
  15.104 -val any = "any";
  15.105 -val anyT = Type (any, []);
  15.106 -
  15.107 -val default_root =
  15.108 -  Config.string (Config.declare "Syntax.default_root" (K (Config.String any)));
  15.109 -
  15.110 -
  15.111 -
  15.112 -(** datatype xprod **)
  15.113 -
  15.114 -(*Delim s: delimiter s
  15.115 -  Argument (s, p): nonterminal s requiring priority >= p, or valued token
  15.116 -  Space s: some white space for printing
  15.117 -  Bg, Brk, En: blocks and breaks for pretty printing*)
  15.118 -
  15.119 -datatype xsymb =
  15.120 -  Delim of string |
  15.121 -  Argument of string * int |
  15.122 -  Space of string |
  15.123 -  Bg of int | Brk of int | En;
  15.124 -
  15.125 -fun is_delim (Delim _) = true
  15.126 -  | is_delim _ = false;
  15.127 -
  15.128 -fun is_terminal (Delim _) = true
  15.129 -  | is_terminal (Argument (s, _)) = Lexicon.is_terminal s
  15.130 -  | is_terminal _ = false;
  15.131 -
  15.132 -fun is_argument (Argument _) = true
  15.133 -  | is_argument _ = false;
  15.134 -
  15.135 -fun is_index (Argument ("index", _)) = true
  15.136 -  | is_index _ = false;
  15.137 -
  15.138 -val index = Argument ("index", 1000);
  15.139 -
  15.140 -
  15.141 -(*XProd (lhs, syms, c, p):
  15.142 -    lhs: name of nonterminal on the lhs of the production
  15.143 -    syms: list of symbols on the rhs of the production
  15.144 -    c: head of parse tree
  15.145 -    p: priority of this production*)
  15.146 -
  15.147 -datatype xprod = XProd of string * xsymb list * string * int;
  15.148 -
  15.149 -val max_pri = 1000;   (*maximum legal priority*)
  15.150 -val chain_pri = ~1;   (*dummy for chain productions*)
  15.151 -
  15.152 -fun delims_of xprods =
  15.153 -  fold (fn XProd (_, xsymbs, _, _) =>
  15.154 -    fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
  15.155 -  |> map Symbol.explode;
  15.156 -
  15.157 -
  15.158 -
  15.159 -(** datatype mfix **)
  15.160 -
  15.161 -(*Mfix (sy, ty, c, ps, p):
  15.162 -    sy: rhs of production as symbolic string
  15.163 -    ty: type description of production
  15.164 -    c: head of parse tree
  15.165 -    ps: priorities of arguments in sy
  15.166 -    p: priority of production*)
  15.167 -
  15.168 -datatype mfix = Mfix of string * typ * string * int list * int;
  15.169 -
  15.170 -fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
  15.171 -  cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
  15.172 -
  15.173 -
  15.174 -(* typ_to_nonterm *)
  15.175 -
  15.176 -fun typ_to_nt _ (Type (c, _)) = c
  15.177 -  | typ_to_nt default _ = default;
  15.178 -
  15.179 -(*get nonterminal for rhs*)
  15.180 -val typ_to_nonterm = typ_to_nt any;
  15.181 -
  15.182 -(*get nonterminal for lhs*)
  15.183 -val typ_to_nonterm1 = typ_to_nt logic;
  15.184 -
  15.185 -
  15.186 -(* read mixfix annotations *)
  15.187 -
  15.188 -local
  15.189 -
  15.190 -val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
  15.191 -
  15.192 -val scan_delim_char =
  15.193 -  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
  15.194 -  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
  15.195 -
  15.196 -fun read_int ["0", "0"] = ~1
  15.197 -  | read_int cs = #1 (Library.read_int cs);
  15.198 -
  15.199 -val scan_sym =
  15.200 -  $$ "_" >> K (Argument ("", 0)) ||
  15.201 -  $$ "\\<index>" >> K index ||
  15.202 -  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
  15.203 -  $$ ")" >> K En ||
  15.204 -  $$ "/" -- $$ "/" >> K (Brk ~1) ||
  15.205 -  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
  15.206 -  Scan.many1 Symbol.is_blank >> (Space o implode) ||
  15.207 -  Scan.repeat1 scan_delim_char >> (Delim o implode);
  15.208 -
  15.209 -val scan_symb =
  15.210 -  scan_sym >> SOME ||
  15.211 -  $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
  15.212 -
  15.213 -val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
  15.214 -val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
  15.215 -
  15.216 -fun unique_index xsymbs =
  15.217 -  if length (filter is_index xsymbs) <= 1 then xsymbs
  15.218 -  else error "Duplicate index arguments (\\<index>)";
  15.219 -
  15.220 -in
  15.221 -
  15.222 -val read_mfix = unique_index o read_symbs o Symbol.explode;
  15.223 -
  15.224 -fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
  15.225 -val mfix_args = length o filter is_argument o read_mfix;
  15.226 -
  15.227 -val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
  15.228 -
  15.229 -end;
  15.230 -
  15.231 -
  15.232 -(* mfix_to_xprod *)
  15.233 -
  15.234 -fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
  15.235 -  let
  15.236 -    fun check_pri p =
  15.237 -      if p >= 0 andalso p <= max_pri then ()
  15.238 -      else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
  15.239 -
  15.240 -    fun blocks_ok [] 0 = true
  15.241 -      | blocks_ok [] _ = false
  15.242 -      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
  15.243 -      | blocks_ok (En :: _) 0 = false
  15.244 -      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
  15.245 -      | blocks_ok (_ :: syms) n = blocks_ok syms n;
  15.246 -
  15.247 -    fun check_blocks syms =
  15.248 -      if blocks_ok syms 0 then ()
  15.249 -      else err_in_mfix "Unbalanced block parentheses" mfix;
  15.250 -
  15.251 -
  15.252 -    val cons_fst = apfst o cons;
  15.253 -
  15.254 -    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
  15.255 -      | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
  15.256 -      | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
  15.257 -          cons_fst arg (add_args syms ty ps)
  15.258 -      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
  15.259 -          cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
  15.260 -      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
  15.261 -          cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
  15.262 -      | add_args (Argument _ :: _) _ _ =
  15.263 -          err_in_mfix "More arguments than in corresponding type" mfix
  15.264 -      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
  15.265 -
  15.266 -    fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
  15.267 -      | rem_pri sym = sym;
  15.268 -
  15.269 -    fun logify_types (a as (Argument (s, p))) =
  15.270 -          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
  15.271 -      | logify_types a = a;
  15.272 -
  15.273 -
  15.274 -    val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
  15.275 -    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
  15.276 -    val (const', typ', parse_rules) =
  15.277 -      if not (exists is_index args) then (const, typ, [])
  15.278 -      else
  15.279 -        let
  15.280 -          val indexed_const =
  15.281 -            if const <> "" then const ^ "_indexed"
  15.282 -            else err_in_mfix "Missing constant name for indexed syntax" mfix;
  15.283 -          val rangeT = Term.range_type typ handle Match =>
  15.284 -            err_in_mfix "Missing structure argument for indexed syntax" mfix;
  15.285 -
  15.286 -          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
  15.287 -          val (xs1, xs2) = chop (find_index is_index args) xs;
  15.288 -          val i = Ast.Variable "i";
  15.289 -          val lhs = Ast.mk_appl (Ast.Constant indexed_const)
  15.290 -            (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
  15.291 -          val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
  15.292 -        in (indexed_const, rangeT, [(lhs, rhs)]) end;
  15.293 -
  15.294 -    val (symbs, lhs) = add_args raw_symbs typ' pris;
  15.295 -
  15.296 -    val copy_prod =
  15.297 -      (lhs = "prop" orelse lhs = "logic")
  15.298 -        andalso const <> ""
  15.299 -        andalso not (null symbs)
  15.300 -        andalso not (exists is_delim symbs);
  15.301 -    val lhs' =
  15.302 -      if convert andalso not copy_prod then
  15.303 -       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
  15.304 -      else lhs;
  15.305 -    val symbs' = map logify_types symbs;
  15.306 -    val xprod = XProd (lhs', symbs', const', pri);
  15.307 -
  15.308 -    val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
  15.309 -    val xprod' =
  15.310 -      if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
  15.311 -      else if const <> "" then xprod
  15.312 -      else if length (filter is_argument symbs') <> 1 then
  15.313 -        err_in_mfix "Copy production must have exactly one argument" mfix
  15.314 -      else if exists is_terminal symbs' then xprod
  15.315 -      else XProd (lhs', map rem_pri symbs', "", chain_pri);
  15.316 -
  15.317 -  in (xprod', parse_rules) end;
  15.318 -
  15.319 -
  15.320 -
  15.321 -(** datatype syn_ext **)
  15.322 -
  15.323 -datatype syn_ext =
  15.324 -  Syn_Ext of {
  15.325 -    xprods: xprod list,
  15.326 -    consts: string list,
  15.327 -    parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
  15.328 -    parse_rules: (Ast.ast * Ast.ast) list,
  15.329 -    parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
  15.330 -    print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
  15.331 -    print_rules: (Ast.ast * Ast.ast) list,
  15.332 -    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list};
  15.333 -
  15.334 -
  15.335 -(* syn_ext *)
  15.336 -
  15.337 -fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) =
  15.338 -  let
  15.339 -    val (parse_ast_translation, parse_translation, print_translation,
  15.340 -      print_ast_translation) = trfuns;
  15.341 -
  15.342 -    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
  15.343 -      |> split_list |> apsnd (rev o flat);
  15.344 -    val mfix_consts =
  15.345 -      distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
  15.346 -  in
  15.347 -    Syn_Ext {
  15.348 -      xprods = xprods,
  15.349 -      consts = union (op =) consts mfix_consts,
  15.350 -      parse_ast_translation = parse_ast_translation,
  15.351 -      parse_rules = parse_rules' @ parse_rules,
  15.352 -      parse_translation = parse_translation,
  15.353 -      print_translation = print_translation,
  15.354 -      print_rules = map swap parse_rules' @ print_rules,
  15.355 -      print_ast_translation = print_ast_translation}
  15.356 -  end;
  15.357 -
  15.358 -
  15.359 -val syn_ext = syn_ext' true (K false);
  15.360 -
  15.361 -fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
  15.362 -fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
  15.363 -fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
  15.364 -
  15.365 -fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
  15.366 -  let fun simple (name, (f, s)) = (name, (K f, s)) in
  15.367 -    syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
  15.368 -  end;
  15.369 -
  15.370 -fun stamp_trfun s (c, f) = (c, (f, s));
  15.371 -fun mk_trfun tr = stamp_trfun (stamp ()) tr;
  15.372 -fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
  15.373 -
  15.374 -
  15.375 -(* pure_ext *)
  15.376 -
  15.377 -val token_markers =
  15.378 -  ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
  15.379 -
  15.380 -val pure_ext = syn_ext' false (K false)
  15.381 -  [Mfix ("_", spropT --> propT, "", [0], 0),
  15.382 -   Mfix ("_", logicT --> anyT, "", [0], 0),
  15.383 -   Mfix ("_", spropT --> anyT, "", [0], 0),
  15.384 -   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
  15.385 -   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
  15.386 -   Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
  15.387 -   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
  15.388 -  token_markers
  15.389 -  ([], [], [], [])
  15.390 -  ([], []);
  15.391 -
  15.392 -end;
    16.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 14:20:57 2011 +0200
    16.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 15:02:11 2011 +0200
    16.3 @@ -13,8 +13,9 @@
    16.4  signature SYNTAX =
    16.5  sig
    16.6    include LEXICON0
    16.7 -  include SYN_EXT0
    16.8    include PRINTER0
    16.9 +  val max_pri: int
   16.10 +  val root: string Config.T
   16.11    val positions_raw: Config.raw
   16.12    val positions: bool Config.T
   16.13    val ambiguity_enabled: bool Config.T
   16.14 @@ -146,10 +147,15 @@
   16.15  structure Syntax: SYNTAX =
   16.16  struct
   16.17  
   16.18 +val max_pri = Syntax_Ext.max_pri;
   16.19 +
   16.20 +
   16.21  (** inner syntax operations **)
   16.22  
   16.23  (* configuration options *)
   16.24  
   16.25 +val root = Config.string (Config.declare "syntax_root" (K (Config.String Syntax_Ext.any)));
   16.26 +
   16.27  val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
   16.28  val positions = Config.bool positions_raw;
   16.29  
   16.30 @@ -403,12 +409,12 @@
   16.31  
   16.32  fun lookup_tr tab c = Option.map fst (Symtab.lookup tab c);
   16.33  
   16.34 -fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
   16.35 +fun remove_trtab trfuns = fold (Symtab.remove Syntax_Ext.eq_trfun) trfuns;
   16.36  
   16.37  fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
   16.38    handle Symtab.DUP c => err_dup_trfun name c;
   16.39  
   16.40 -fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
   16.41 +fun merge_trtabs name tab1 tab2 = Symtab.merge Syntax_Ext.eq_trfun (tab1, tab2)
   16.42    handle Symtab.DUP c => err_dup_trfun name c;
   16.43  
   16.44  
   16.45 @@ -428,9 +434,9 @@
   16.46        | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
   16.47    in app_first fns end;
   16.48  
   16.49 -fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
   16.50 -fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
   16.51 -fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
   16.52 +fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syntax_Ext.eq_trfun) trfuns;
   16.53 +fun remove_tr'tab trfuns = fold (Symtab.remove_list Syntax_Ext.eq_trfun) trfuns;
   16.54 +fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syntax_Ext.eq_trfun (tab1, tab2);
   16.55  
   16.56  
   16.57  
   16.58 @@ -450,7 +456,7 @@
   16.59  
   16.60  datatype syntax =
   16.61    Syntax of {
   16.62 -    input: Syn_Ext.xprod list,
   16.63 +    input: Syntax_Ext.xprod list,
   16.64      lexicon: Scan.lexicon,
   16.65      gram: Parser.gram,
   16.66      consts: string list,
   16.67 @@ -508,7 +514,7 @@
   16.68    let
   16.69      val {input, lexicon, gram, consts = consts1, prmodes, parse_ast_trtab, parse_ruletab,
   16.70        parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs;
   16.71 -    val Syn_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation,
   16.72 +    val Syntax_Ext.Syn_Ext {xprods, consts = consts2, parse_ast_translation,
   16.73        parse_rules, parse_translation, print_translation, print_rules,
   16.74        print_ast_translation} = syn_ext;
   16.75      val new_xprods =
   16.76 @@ -517,7 +523,7 @@
   16.77    in
   16.78      Syntax
   16.79      ({input = new_xprods @ input,
   16.80 -      lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
   16.81 +      lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
   16.82        gram = Parser.extend_gram new_xprods gram,
   16.83        consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
   16.84        prmodes = insert (op =) mode prmodes,
   16.85 @@ -536,7 +542,7 @@
   16.86  
   16.87  fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   16.88    let
   16.89 -    val Syn_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules,
   16.90 +    val Syntax_Ext.Syn_Ext {xprods, consts = _, parse_ast_translation, parse_rules,
   16.91        parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext;
   16.92      val {input, lexicon, gram, consts, prmodes, parse_ast_trtab, parse_ruletab,
   16.93        parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs;
   16.94 @@ -546,7 +552,7 @@
   16.95    in
   16.96      Syntax
   16.97      ({input = input',
   16.98 -      lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
   16.99 +      lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon,
  16.100        gram = if changed then Parser.extend_gram input' Parser.empty_gram else gram,
  16.101        consts = consts,
  16.102        prmodes = prmodes,
  16.103 @@ -593,12 +599,12 @@
  16.104  
  16.105  (* basic syntax *)
  16.106  
  16.107 -val basic_syntax = update_syntax mode_default Syn_Ext.pure_ext empty_syntax;
  16.108 +val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax;
  16.109  
  16.110  val basic_nonterms =
  16.111 -  (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
  16.112 -    Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
  16.113 -    "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const", "index",
  16.114 +  (Lexicon.terminals @ [Syntax_Ext.logic, "type", "types", "sort", "classes",
  16.115 +    Syntax_Ext.args, Syntax_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
  16.116 +    "asms", Syntax_Ext.any, Syntax_Ext.sprop, "num_const", "float_const", "index",
  16.117      "struct", "id_position", "longid_position", "type_name", "class_name"]);
  16.118  
  16.119  
  16.120 @@ -708,8 +714,8 @@
  16.121  
  16.122  fun ext_syntax f decls = update_syntax mode_default (f decls);
  16.123  
  16.124 -val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
  16.125 -val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
  16.126 +val update_trfuns = ext_syntax Syntax_Ext.syn_ext_trfuns;
  16.127 +val update_advanced_trfuns = ext_syntax Syntax_Ext.syn_ext_advanced_trfuns;
  16.128  
  16.129  fun update_type_gram add prmode decls =
  16.130    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
  16.131 @@ -717,13 +723,13 @@
  16.132  fun update_const_gram add is_logtype prmode decls =
  16.133    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
  16.134  
  16.135 -val update_trrules = ext_syntax Syn_Ext.syn_ext_rules o check_rules;
  16.136 -val remove_trrules = remove_syntax mode_default o Syn_Ext.syn_ext_rules o check_rules;
  16.137 +val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
  16.138 +val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
  16.139  
  16.140  
  16.141  (*export parts of internal Syntax structures*)
  16.142  val syntax_tokenize = tokenize;
  16.143 -open Lexicon Syn_Ext Printer;
  16.144 +open Lexicon Printer;
  16.145  val tokenize = syntax_tokenize;
  16.146  
  16.147  end;
  16.148 @@ -731,5 +737,3 @@
  16.149  structure Basic_Syntax: BASIC_SYNTAX = Syntax;
  16.150  open Basic_Syntax;
  16.151  
  16.152 -forget_structure "Syn_Ext";
  16.153 -
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 15:02:11 2011 +0200
    17.3 @@ -0,0 +1,380 @@
    17.4 +(*  Title:      Pure/Syntax/syntax_ext.ML
    17.5 +    Author:     Markus Wenzel and Carsten Clasohm, TU Muenchen
    17.6 +
    17.7 +Syntax extension.
    17.8 +*)
    17.9 +
   17.10 +signature SYNTAX_EXT =
   17.11 +sig
   17.12 +  val dddot_indexname: indexname
   17.13 +  val logic: string
   17.14 +  val args: string
   17.15 +  val cargs: string
   17.16 +  val typeT: typ
   17.17 +  val any: string
   17.18 +  val sprop: string
   17.19 +  val spropT: typ
   17.20 +  val max_pri: int
   17.21 +  datatype mfix = Mfix of string * typ * string * int list * int
   17.22 +  val err_in_mfix: string -> mfix -> 'a
   17.23 +  val typ_to_nonterm: typ -> string
   17.24 +  datatype xsymb =
   17.25 +    Delim of string |
   17.26 +    Argument of string * int |
   17.27 +    Space of string |
   17.28 +    Bg of int | Brk of int | En
   17.29 +  datatype xprod = XProd of string * xsymb list * string * int
   17.30 +  val chain_pri: int
   17.31 +  val delims_of: xprod list -> string list list
   17.32 +  datatype syn_ext =
   17.33 +    Syn_Ext of {
   17.34 +      xprods: xprod list,
   17.35 +      consts: string list,
   17.36 +      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
   17.37 +      parse_rules: (Ast.ast * Ast.ast) list,
   17.38 +      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
   17.39 +      print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
   17.40 +      print_rules: (Ast.ast * Ast.ast) list,
   17.41 +      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
   17.42 +  val mfix_delims: string -> string list
   17.43 +  val mfix_args: string -> int
   17.44 +  val escape: string -> string
   17.45 +  val syn_ext': bool -> (string -> bool) -> mfix list ->
   17.46 +    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   17.47 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
   17.48 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   17.49 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
   17.50 +    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   17.51 +  val syn_ext: mfix list -> string list ->
   17.52 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   17.53 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
   17.54 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   17.55 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
   17.56 +    (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   17.57 +  val syn_ext_const_names: string list -> syn_ext
   17.58 +  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   17.59 +  val syn_ext_trfuns:
   17.60 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list *
   17.61 +    (string * ((term list -> term) * stamp)) list *
   17.62 +    (string * ((typ -> term list -> term) * stamp)) list *
   17.63 +    (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   17.64 +  val syn_ext_advanced_trfuns:
   17.65 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
   17.66 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
   17.67 +    (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
   17.68 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   17.69 +  val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
   17.70 +  val mk_trfun: string * 'a -> string * ('a * stamp)
   17.71 +  val eq_trfun: ('a * stamp) * ('a * stamp) -> bool
   17.72 +  val token_markers: string list
   17.73 +  val pure_ext: syn_ext
   17.74 +end;
   17.75 +
   17.76 +structure Syntax_Ext: SYNTAX_EXT =
   17.77 +struct
   17.78 +
   17.79 +
   17.80 +(** misc definitions **)
   17.81 +
   17.82 +val dddot_indexname = ("dddot", 0);
   17.83 +
   17.84 +
   17.85 +(* syntactic categories *)
   17.86 +
   17.87 +val logic = "logic";
   17.88 +val logicT = Type (logic, []);
   17.89 +
   17.90 +val args = "args";
   17.91 +val cargs = "cargs";
   17.92 +
   17.93 +val typeT = Type ("type", []);
   17.94 +
   17.95 +val sprop = "#prop";
   17.96 +val spropT = Type (sprop, []);
   17.97 +
   17.98 +val any = "any";
   17.99 +val anyT = Type (any, []);
  17.100 +
  17.101 +
  17.102 +
  17.103 +(** datatype xprod **)
  17.104 +
  17.105 +(*Delim s: delimiter s
  17.106 +  Argument (s, p): nonterminal s requiring priority >= p, or valued token
  17.107 +  Space s: some white space for printing
  17.108 +  Bg, Brk, En: blocks and breaks for pretty printing*)
  17.109 +
  17.110 +datatype xsymb =
  17.111 +  Delim of string |
  17.112 +  Argument of string * int |
  17.113 +  Space of string |
  17.114 +  Bg of int | Brk of int | En;
  17.115 +
  17.116 +fun is_delim (Delim _) = true
  17.117 +  | is_delim _ = false;
  17.118 +
  17.119 +fun is_terminal (Delim _) = true
  17.120 +  | is_terminal (Argument (s, _)) = Lexicon.is_terminal s
  17.121 +  | is_terminal _ = false;
  17.122 +
  17.123 +fun is_argument (Argument _) = true
  17.124 +  | is_argument _ = false;
  17.125 +
  17.126 +fun is_index (Argument ("index", _)) = true
  17.127 +  | is_index _ = false;
  17.128 +
  17.129 +val index = Argument ("index", 1000);
  17.130 +
  17.131 +
  17.132 +(*XProd (lhs, syms, c, p):
  17.133 +    lhs: name of nonterminal on the lhs of the production
  17.134 +    syms: list of symbols on the rhs of the production
  17.135 +    c: head of parse tree
  17.136 +    p: priority of this production*)
  17.137 +
  17.138 +datatype xprod = XProd of string * xsymb list * string * int;
  17.139 +
  17.140 +val max_pri = 1000;   (*maximum legal priority*)
  17.141 +val chain_pri = ~1;   (*dummy for chain productions*)
  17.142 +
  17.143 +fun delims_of xprods =
  17.144 +  fold (fn XProd (_, xsymbs, _, _) =>
  17.145 +    fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
  17.146 +  |> map Symbol.explode;
  17.147 +
  17.148 +
  17.149 +
  17.150 +(** datatype mfix **)
  17.151 +
  17.152 +(*Mfix (sy, ty, c, ps, p):
  17.153 +    sy: rhs of production as symbolic string
  17.154 +    ty: type description of production
  17.155 +    c: head of parse tree
  17.156 +    ps: priorities of arguments in sy
  17.157 +    p: priority of production*)
  17.158 +
  17.159 +datatype mfix = Mfix of string * typ * string * int list * int;
  17.160 +
  17.161 +fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
  17.162 +  cat_error msg ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
  17.163 +
  17.164 +
  17.165 +(* typ_to_nonterm *)
  17.166 +
  17.167 +fun typ_to_nt _ (Type (c, _)) = c
  17.168 +  | typ_to_nt default _ = default;
  17.169 +
  17.170 +(*get nonterminal for rhs*)
  17.171 +val typ_to_nonterm = typ_to_nt any;
  17.172 +
  17.173 +(*get nonterminal for lhs*)
  17.174 +val typ_to_nonterm1 = typ_to_nt logic;
  17.175 +
  17.176 +
  17.177 +(* read mixfix annotations *)
  17.178 +
  17.179 +local
  17.180 +
  17.181 +val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
  17.182 +
  17.183 +val scan_delim_char =
  17.184 +  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.is_regular) ||
  17.185 +  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.is_regular);
  17.186 +
  17.187 +fun read_int ["0", "0"] = ~1
  17.188 +  | read_int cs = #1 (Library.read_int cs);
  17.189 +
  17.190 +val scan_sym =
  17.191 +  $$ "_" >> K (Argument ("", 0)) ||
  17.192 +  $$ "\\<index>" >> K index ||
  17.193 +  $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
  17.194 +  $$ ")" >> K En ||
  17.195 +  $$ "/" -- $$ "/" >> K (Brk ~1) ||
  17.196 +  $$ "/" |-- Scan.many Symbol.is_blank >> (Brk o length) ||
  17.197 +  Scan.many1 Symbol.is_blank >> (Space o implode) ||
  17.198 +  Scan.repeat1 scan_delim_char >> (Delim o implode);
  17.199 +
  17.200 +val scan_symb =
  17.201 +  scan_sym >> SOME ||
  17.202 +  $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
  17.203 +
  17.204 +val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'");
  17.205 +val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs;
  17.206 +
  17.207 +fun unique_index xsymbs =
  17.208 +  if length (filter is_index xsymbs) <= 1 then xsymbs
  17.209 +  else error "Duplicate index arguments (\\<index>)";
  17.210 +
  17.211 +in
  17.212 +
  17.213 +val read_mfix = unique_index o read_symbs o Symbol.explode;
  17.214 +
  17.215 +fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
  17.216 +val mfix_args = length o filter is_argument o read_mfix;
  17.217 +
  17.218 +val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
  17.219 +
  17.220 +end;
  17.221 +
  17.222 +
  17.223 +(* mfix_to_xprod *)
  17.224 +
  17.225 +fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
  17.226 +  let
  17.227 +    fun check_pri p =
  17.228 +      if p >= 0 andalso p <= max_pri then ()
  17.229 +      else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
  17.230 +
  17.231 +    fun blocks_ok [] 0 = true
  17.232 +      | blocks_ok [] _ = false
  17.233 +      | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1)
  17.234 +      | blocks_ok (En :: _) 0 = false
  17.235 +      | blocks_ok (En :: syms) n = blocks_ok syms (n - 1)
  17.236 +      | blocks_ok (_ :: syms) n = blocks_ok syms n;
  17.237 +
  17.238 +    fun check_blocks syms =
  17.239 +      if blocks_ok syms 0 then ()
  17.240 +      else err_in_mfix "Unbalanced block parentheses" mfix;
  17.241 +
  17.242 +
  17.243 +    val cons_fst = apfst o cons;
  17.244 +
  17.245 +    fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
  17.246 +      | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
  17.247 +      | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
  17.248 +          cons_fst arg (add_args syms ty ps)
  17.249 +      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
  17.250 +          cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
  17.251 +      | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
  17.252 +          cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
  17.253 +      | add_args (Argument _ :: _) _ _ =
  17.254 +          err_in_mfix "More arguments than in corresponding type" mfix
  17.255 +      | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
  17.256 +
  17.257 +    fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
  17.258 +      | rem_pri sym = sym;
  17.259 +
  17.260 +    fun logify_types (a as (Argument (s, p))) =
  17.261 +          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
  17.262 +      | logify_types a = a;
  17.263 +
  17.264 +
  17.265 +    val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
  17.266 +    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
  17.267 +    val (const', typ', parse_rules) =
  17.268 +      if not (exists is_index args) then (const, typ, [])
  17.269 +      else
  17.270 +        let
  17.271 +          val indexed_const =
  17.272 +            if const <> "" then const ^ "_indexed"
  17.273 +            else err_in_mfix "Missing constant name for indexed syntax" mfix;
  17.274 +          val rangeT = Term.range_type typ handle Match =>
  17.275 +            err_in_mfix "Missing structure argument for indexed syntax" mfix;
  17.276 +
  17.277 +          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
  17.278 +          val (xs1, xs2) = chop (find_index is_index args) xs;
  17.279 +          val i = Ast.Variable "i";
  17.280 +          val lhs = Ast.mk_appl (Ast.Constant indexed_const)
  17.281 +            (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
  17.282 +          val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
  17.283 +        in (indexed_const, rangeT, [(lhs, rhs)]) end;
  17.284 +
  17.285 +    val (symbs, lhs) = add_args raw_symbs typ' pris;
  17.286 +
  17.287 +    val copy_prod =
  17.288 +      (lhs = "prop" orelse lhs = "logic")
  17.289 +        andalso const <> ""
  17.290 +        andalso not (null symbs)
  17.291 +        andalso not (exists is_delim symbs);
  17.292 +    val lhs' =
  17.293 +      if convert andalso not copy_prod then
  17.294 +       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
  17.295 +      else lhs;
  17.296 +    val symbs' = map logify_types symbs;
  17.297 +    val xprod = XProd (lhs', symbs', const', pri);
  17.298 +
  17.299 +    val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs');
  17.300 +    val xprod' =
  17.301 +      if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
  17.302 +      else if const <> "" then xprod
  17.303 +      else if length (filter is_argument symbs') <> 1 then
  17.304 +        err_in_mfix "Copy production must have exactly one argument" mfix
  17.305 +      else if exists is_terminal symbs' then xprod
  17.306 +      else XProd (lhs', map rem_pri symbs', "", chain_pri);
  17.307 +
  17.308 +  in (xprod', parse_rules) end;
  17.309 +
  17.310 +
  17.311 +
  17.312 +(** datatype syn_ext **)
  17.313 +
  17.314 +datatype syn_ext =
  17.315 +  Syn_Ext of {
  17.316 +    xprods: xprod list,
  17.317 +    consts: string list,
  17.318 +    parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
  17.319 +    parse_rules: (Ast.ast * Ast.ast) list,
  17.320 +    parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
  17.321 +    print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
  17.322 +    print_rules: (Ast.ast * Ast.ast) list,
  17.323 +    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list};
  17.324 +
  17.325 +
  17.326 +(* syn_ext *)
  17.327 +
  17.328 +fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) =
  17.329 +  let
  17.330 +    val (parse_ast_translation, parse_translation, print_translation,
  17.331 +      print_ast_translation) = trfuns;
  17.332 +
  17.333 +    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
  17.334 +      |> split_list |> apsnd (rev o flat);
  17.335 +    val mfix_consts =
  17.336 +      distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
  17.337 +  in
  17.338 +    Syn_Ext {
  17.339 +      xprods = xprods,
  17.340 +      consts = union (op =) consts mfix_consts,
  17.341 +      parse_ast_translation = parse_ast_translation,
  17.342 +      parse_rules = parse_rules' @ parse_rules,
  17.343 +      parse_translation = parse_translation,
  17.344 +      print_translation = print_translation,
  17.345 +      print_rules = map swap parse_rules' @ print_rules,
  17.346 +      print_ast_translation = print_ast_translation}
  17.347 +  end;
  17.348 +
  17.349 +
  17.350 +val syn_ext = syn_ext' true (K false);
  17.351 +
  17.352 +fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
  17.353 +fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
  17.354 +fun syn_ext_advanced_trfuns trfuns = syn_ext [] [] trfuns ([], []);
  17.355 +
  17.356 +fun syn_ext_trfuns (atrs, trs, tr's, atr's) =
  17.357 +  let fun simple (name, (f, s)) = (name, (K f, s)) in
  17.358 +    syn_ext_advanced_trfuns (map simple atrs, map simple trs, map simple tr's, map simple atr's)
  17.359 +  end;
  17.360 +
  17.361 +fun stamp_trfun s (c, f) = (c, (f, s));
  17.362 +fun mk_trfun tr = stamp_trfun (stamp ()) tr;
  17.363 +fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
  17.364 +
  17.365 +
  17.366 +(* pure_ext *)
  17.367 +
  17.368 +val token_markers =
  17.369 +  ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
  17.370 +
  17.371 +val pure_ext = syn_ext' false (K false)
  17.372 +  [Mfix ("_", spropT --> propT, "", [0], 0),
  17.373 +   Mfix ("_", logicT --> anyT, "", [0], 0),
  17.374 +   Mfix ("_", spropT --> anyT, "", [0], 0),
  17.375 +   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
  17.376 +   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
  17.377 +   Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
  17.378 +   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
  17.379 +  token_markers
  17.380 +  ([], [], [], [])
  17.381 +  ([], []);
  17.382 +
  17.383 +end;
    18.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 14:20:57 2011 +0200
    18.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:02:11 2011 +0200
    18.3 @@ -330,7 +330,7 @@
    18.4      val (markup, kind, root, constrain) =
    18.5        if is_prop
    18.6        then (Markup.prop, "proposition", "prop", Type.constraint propT)
    18.7 -      else (Markup.term, "term", Config.get ctxt Syntax.default_root, I);
    18.8 +      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
    18.9      val (syms, pos) = Syntax.parse_token ctxt markup text;
   18.10    in
   18.11      let
   18.12 @@ -491,7 +491,7 @@
   18.13      val {structs, fixes} = idents;
   18.14  
   18.15      fun mark_atoms ((t as Const (c, _)) $ u) =
   18.16 -          if member (op =) Syntax.token_markers c
   18.17 +          if member (op =) Syntax_Ext.token_markers c
   18.18            then t $ u else mark_atoms t $ mark_atoms u
   18.19        | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
   18.20        | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
   18.21 @@ -507,7 +507,7 @@
   18.22              else Lexicon.const "_free" $ t
   18.23            end
   18.24        | mark_atoms (t as Var (xi, T)) =
   18.25 -          if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
   18.26 +          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
   18.27            else Lexicon.const "_var" $ t
   18.28        | mark_atoms a = a;
   18.29  
    19.1 --- a/src/Pure/Syntax/syntax_trans.ML	Fri Apr 08 14:20:57 2011 +0200
    19.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Fri Apr 08 15:02:11 2011 +0200
    19.3 @@ -185,7 +185,7 @@
    19.4  
    19.5  (* dddot *)
    19.6  
    19.7 -fun dddot_tr ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
    19.8 +fun dddot_tr ts = Term.list_comb (Lexicon.var Syntax_Ext.dddot_indexname, ts);
    19.9  
   19.10  
   19.11  (* quote / antiquote *)
    20.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 14:20:57 2011 +0200
    20.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 15:02:11 2011 +0200
    20.3 @@ -19,8 +19,8 @@
    20.4  val tycon = Syntax.mark_type;
    20.5  val const = Syntax.mark_const;
    20.6  
    20.7 -val typeT = Syntax.typeT;
    20.8 -val spropT = Syntax.spropT;
    20.9 +val typeT = Syntax_Ext.typeT;
   20.10 +val spropT = Syntax_Ext.spropT;
   20.11  
   20.12  
   20.13  (* application syntax variants *)
    21.1 --- a/src/Pure/sign.ML	Fri Apr 08 14:20:57 2011 +0200
    21.2 +++ b/src/Pure/sign.ML	Fri Apr 08 15:02:11 2011 +0200
    21.3 @@ -468,7 +468,7 @@
    21.4  
    21.5  local
    21.6  
    21.7 -fun mk trs = map Syntax.mk_trfun trs;
    21.8 +fun mk trs = map Syntax_Ext.mk_trfun trs;
    21.9  
   21.10  fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) =
   21.11    map_syn (ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's));