# HG changeset patch
# User wenzelm
# Date 1165683948 -3600
# Node ID 906649272ba0dff60e5b40f63c2dd1a4eb559103
# Parent  5acd4f35d26fee4832fa3056ae218b71a59931ba
added read/pretty_term_abbrev, print_abbrevs;
tuned Consts signature;
renamed expand_abbrevs to set_expand_abbrevs;

diff -r 5acd4f35d26f -r 906649272ba0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Dec 09 18:05:47 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Dec 09 18:05:48 2006 +0100
@@ -25,6 +25,7 @@
   val theory: (theory -> theory) -> Proof.context -> Proof.context
   val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val pretty_term: Proof.context -> term -> Pretty.T
+  val pretty_term_abbrev: Proof.context -> term -> Pretty.T
   val pretty_typ: Proof.context -> typ -> Pretty.T
   val pretty_sort: Proof.context -> sort -> Pretty.T
   val pretty_classrel: Proof.context -> class list -> Pretty.T
@@ -60,6 +61,7 @@
   val read_prop_schematic: Proof.context -> string -> term
   val read_term_pats: typ -> Proof.context -> string list -> term list
   val read_prop_pats: Proof.context -> string list -> term list
+  val read_term_abbrev: Proof.context -> string -> term
   val cert_term: Proof.context -> term -> term
   val cert_prop: Proof.context -> term -> term
   val cert_term_pats: typ -> Proof.context -> term list -> term list
@@ -106,6 +108,7 @@
   val qualified_names: Proof.context -> Proof.context
   val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
+  val reset_naming: Proof.context -> Proof.context
   val hide_thms: bool -> string list -> Proof.context -> Proof.context
   val put_thms: string * thm list option -> Proof.context -> Proof.context
   val note_thmss: string ->
@@ -141,12 +144,13 @@
   val get_case: Proof.context -> string -> string option list -> RuleCases.T
   val add_notation: Syntax.mode -> (term * mixfix) list ->
     Proof.context -> Proof.context
-  val expand_abbrevs: bool -> Proof.context -> Proof.context
+  val set_expand_abbrevs: bool -> Proof.context -> Proof.context
   val add_abbrev: string -> bstring * term -> Proof.context ->
     ((string * typ) * term) * Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: Proof.context -> unit
+  val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
   val print_lthms: Proof.context -> unit
   val print_cases: Proof.context -> unit
@@ -281,6 +285,7 @@
     val consts = consts_of ctxt;
     val t' = t
       |> abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (! print_mode @ [""]))
+      |> abbrevs ? rewrite_term thy (Consts.abbrevs_of consts [#1 Syntax.internal_mode])
       |> Sign.extern_term (Consts.extern_early consts) thy
       |> LocalSyntax.extern_term syntax;
   in
@@ -290,7 +295,7 @@
 in
 
 val pretty_term = pretty_term' true;
-val pretty_term_no_abbrevs = pretty_term' false;
+val pretty_term_abbrev = pretty_term' false;
 
 end;
 
@@ -328,7 +333,7 @@
       Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
 
 fun pretty_proof ctxt prf =
-  pretty_term_no_abbrevs (ctxt |> transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt)))
+  pretty_term_abbrev (ctxt |> transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt)))
     (ProofSyntax.term_of_proof prf);
 
 fun pretty_proof_of ctxt full th =
@@ -759,6 +764,7 @@
 val qualified_names = map_naming NameSpace.qualified_names;
 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val restore_naming  = map_naming o K o naming_of;
+val reset_naming    = map_naming (K local_naming);
 
 fun hide_thms fully names = map_thms (fn ((space, tab), index) =>
   ((fold (NameSpace.hide fully) names space, tab), index));
@@ -862,7 +868,7 @@
       let
         val consts = Context.cases Sign.consts_of consts_of context;
         val c' = Consts.intern consts c;
-        val _ = Consts.constraint consts c' handle TYPE (msg, _, _) => error msg;
+        val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
       in Syntax.Constant (Syntax.constN ^ c') end
   | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts);
 
@@ -875,15 +881,16 @@
 
 (* abbreviations *)
 
-val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
+val set_expand_abbrevs = map_consts o apsnd o Consts.set_expand;
+fun read_term_abbrev ctxt = read_term (set_expand_abbrevs false ctxt);
 
 fun add_abbrev mode (c, raw_t) ctxt =
   let
-    val t0 = cert_term (ctxt |> expand_abbrevs false) raw_t
+    val t0 = cert_term (ctxt |> set_expand_abbrevs false) raw_t
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val (res, consts') = consts_of ctxt
-      |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode ((c, t), true);
+      |> Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (c, t);
   in
     ctxt
     |> Variable.declare_term t
@@ -1040,28 +1047,31 @@
 val print_syntax = Syntax.print_syntax o syn_of;
 
 
-(* local consts *)
+(* abbreviations *)
 
-fun pretty_consts ctxt =
+fun pretty_abbrevs show_globals ctxt =
   let
     val ((_, globals), (space, consts)) =
       pairself (#constants o Consts.dest) (#consts (rep_context ctxt));
-    fun local_abbrev (_, (_, NONE)) = I
-      | local_abbrev (c, (T, SOME t)) =
-          if Symtab.defined globals c then I else cons (c, Logic.mk_equals (Const (c, T), t));
-    val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold local_abbrev consts []));
+    fun add_abbrev (_, (_, NONE)) = I
+      | add_abbrev (c, (T, SOME (t, _))) =
+          if not show_globals andalso Symtab.defined globals c then I
+          else cons (c, Logic.mk_equals (Const (c, T), t));
+    val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold add_abbrev consts []));
   in
     if null abbrevs andalso not (! verbose) then []
-    else [Pretty.big_list "abbreviations:" (map (pretty_term_no_abbrevs ctxt o #2) abbrevs)]
+    else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   end;
 
+val print_abbrevs = Pretty.writeln o Pretty.chunks o pretty_abbrevs true;
+
 
 (* term bindings *)
 
 fun pretty_binds ctxt =
   let
     val binds = Variable.binds_of ctxt;
-    fun prt_bind (xi, (T, t)) = pretty_term_no_abbrevs ctxt (Logic.mk_equals (Var (xi, T), t));
+    fun prt_bind (xi, (T, t)) = pretty_term_abbrev ctxt (Logic.mk_equals (Var (xi, T), t));
   in
     if Vartab.is_empty binds andalso not (! verbose) then []
     else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))]
@@ -1190,7 +1200,7 @@
   in
     verb single (K pretty_thy) @
     pretty_ctxt ctxt @
-    verb pretty_consts (K ctxt) @
+    verb (pretty_abbrevs false) (K ctxt) @
     verb pretty_binds (K ctxt) @
     verb pretty_lthms (K ctxt) @
     verb pretty_cases (K ctxt) @