# HG changeset patch
# User wenzelm
# Date 1144529480 -7200
# Node ID a2040baa9444038ec7190b3cdb91ae711becd768
# Parent  4fd1246d7998291f06368a6ed2607536448200a7
pretty_term': early vs. late externing (support authentic syntax);
add_abbrevs(_i): support print mode and authentic syntax;

diff -r 4fd1246d7998 -r a2040baa9444 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Apr 08 22:51:19 2006 +0200
+++ b/src/Pure/sign.ML	Sat Apr 08 22:51:20 2006 +0200
@@ -25,8 +25,8 @@
   val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-  val add_abbrevs: bool -> (bstring * string * mixfix) list -> theory -> theory
-  val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> theory -> theory
+  val add_abbrevs: string * bool -> (bstring * string * mixfix) list -> theory -> theory
+  val add_abbrevs_i: string * bool -> (bstring * term * mixfix) list -> theory -> theory
   val add_const_constraint: xstring * string option -> theory -> theory
   val add_const_constraint_i: string * typ option -> theory -> theory
   val add_classes: (bstring * xstring list) list -> theory -> theory
@@ -136,7 +136,7 @@
   val intern_term: theory -> term -> term
   val extern_term: (string -> xstring) -> theory -> term -> term
   val intern_tycons: theory -> typ -> typ
-  val pretty_term': Syntax.syntax -> Context.generic -> term -> Pretty.T
+  val pretty_term': Context.generic -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T
   val pretty_term: theory -> term -> Pretty.T
   val pretty_typ: theory -> typ -> Pretty.T
   val pretty_sort: theory -> sort -> Pretty.T
@@ -155,7 +155,7 @@
   val certify_typ: theory -> typ -> typ
   val certify_typ_syntax: theory -> typ -> typ
   val certify_typ_abbrev: theory -> typ -> typ
-  val certify: bool -> bool -> Pretty.pp -> theory -> term -> term * typ * int
+  val certify': bool -> bool -> Pretty.pp -> Consts.T -> theory -> term -> term * typ * int
   val certify_term: theory -> term -> term * typ * int
   val certify_prop: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
@@ -370,13 +370,13 @@
 
 (** pretty printing of terms, types etc. **)
 
-fun pretty_term' syn context t =
+fun pretty_term' context syn ext t =
   let val curried = Context.exists_name Context.CPureN (Context.theory_of context)
-  in Syntax.pretty_term context syn curried t end;
+  in Syntax.pretty_term ext context syn curried t end;
 
 fun pretty_term thy t =
-  pretty_term' (syn_of thy) (Context.Theory thy)
-    (extern_term (NameSpace.extern (Consts.space_of (consts_of thy))) thy t);
+  pretty_term' (Context.Theory thy) (syn_of thy) (Consts.extern (consts_of thy))
+    (extern_term (Consts.extern_early (consts_of thy)) thy t);
 
 fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
 fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
@@ -459,20 +459,21 @@
 
 in
 
-fun certify normalize prop pp thy tm =
+fun certify' normalize prop pp consts thy tm =
   let
     val _ = Context.check_thy thy;
     val _ = check_vars tm;
     val tm' = Term.map_term_types (certify_typ thy) tm;
     val T = type_check pp tm';
     val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
-    val tm'' = Consts.certify pp (tsig_of thy) (consts_of thy) tm';
+    val tm'' = Consts.certify pp (tsig_of thy) consts tm';
     val tm'' = if normalize then tm'' else tm';
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
-fun certify_term thy = certify true false (pp thy) thy;
-fun certify_prop thy = certify true true (pp thy) thy;
+fun certify_term thy = certify' true false (pp thy) (consts_of thy) thy;
+fun certify_prop thy = certify' true true (pp thy) (consts_of thy) thy;
 
+fun cert_term_abbrev thy = #1 o certify' false false (pp thy) (consts_of thy) thy;
 val cert_term = #1 oo certify_term;
 val cert_prop = #1 oo certify_prop;
 
@@ -596,8 +597,7 @@
       map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
 
     fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
-        (try (Consts.constraint consts)) def_type def_sort
-        (NameSpace.intern (Consts.space_of consts))
+        (try (Consts.constraint consts)) def_type def_sort (Consts.intern consts)
         (intern_tycons thy) (intern_sort thy) used freeze typs ts)
       handle TYPE (msg, _, _) => Exn (ERROR msg);
 
@@ -745,7 +745,7 @@
       handle ERROR msg =>
         cat_error msg ("in declaration of constant " ^ quote (Syntax.const_name c mx));
     val args = map prep raw_args;
-    val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, T));
+    val decls = args |> map (fn (c, T, mx) => ((Syntax.const_name c mx, T), true));
   in
     thy
     |> map_consts (fold (Consts.declare (naming_of thy)) decls)
@@ -764,27 +764,29 @@
 
 local
 
-fun gen_add_abbrevs prep_term revert raw_args thy =
+fun gen_abbrevs prep_term (mode, inout) = fold (fn (raw_c, raw_t, raw_mx) => fn thy =>
   let
+    val naming = naming_of thy
+      |> K (mode <> "") ? (NameSpace.add_path mode #> NameSpace.no_base_names);
     val prep_tm =
       Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy;
-    fun prep (raw_c, raw_t, mx) =
-      let
-        val c = Syntax.const_name raw_c mx;
-        val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
-          handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
-      in ((c, t), (raw_c, Term.fastype_of t, mx)) end;
-    val (abbrs, syn) = split_list (map prep raw_args);
+
+    val (c, mx) = Syntax.const_mixfix raw_c raw_mx;
+    val (c', b) = Syntax.mixfix_const (NameSpace.full naming c) mx;
+    val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg)
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
+    val T = Term.fastype_of t;
   in
     thy
-    |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) revert) abbrs)
-    |> add_syntax_i syn
-  end;
+    |> map_consts (Consts.abbreviate (pp thy) (tsig_of thy) naming mode ((c, t), b))
+    |> map_syn (Syntax.extend_consts [c])
+    |> add_modesyntax_i (mode, inout) [(c', T, mx)]
+  end);
 
 in
 
-val add_abbrevs = gen_add_abbrevs read_term;
-val add_abbrevs_i = gen_add_abbrevs cert_term;
+val add_abbrevs = gen_abbrevs read_term;
+val add_abbrevs_i = gen_abbrevs cert_term_abbrev;
 
 end;