src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 08 22:51:26 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 08 22:51:28 2006 +0200
@@ -149,8 +149,9 @@
   val add_cases: bool -> (string * RuleCases.T option) list -> context -> context
   val apply_case: RuleCases.T -> context -> (string * term list) list * context
   val get_case: context -> string -> string option list -> RuleCases.T
-  val add_abbrevs: bool -> (bstring * string * mixfix) list -> context -> context
-  val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> context -> context
+  val expand_abbrevs: bool -> context -> context
+  val add_abbrevs: string * bool -> (bstring * string * mixfix) list -> context -> context
+  val add_abbrevs_i: string * bool -> (bstring * term * mixfix) list -> context -> context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
   val print_syntax: context -> unit
@@ -312,15 +313,22 @@
 
 local
 
+fun rewrite_term thy rews t =
+  if can Term.type_of t then Pattern.rewrite_term thy rews [] t
+  else (warning "Printing ill-typed term -- cannot expand abbreviations"; t);
+
 fun pretty_term' abbrevs ctxt t =
   let
     val thy = theory_of ctxt;
     val syntax = syntax_of ctxt;
     val consts = consts_of ctxt;
     val t' = t
-      |> K abbrevs ? Pattern.rewrite_term thy (Consts.abbrevs_of consts) []
-      |> LocalSyntax.extern_term (NameSpace.extern (Consts.space_of consts)) thy syntax;
-  in Sign.pretty_term' (LocalSyntax.syn_of syntax) (Context.Proof ctxt) t' end;
+      |> K abbrevs ? rewrite_term thy (Consts.abbrevs_of consts (! print_mode @ [""]))
+      |> Sign.extern_term (Consts.extern_early consts) thy
+      |> LocalSyntax.extern_term syntax;
+  in
+    Sign.pretty_term' (Context.Proof ctxt) (LocalSyntax.syn_of syntax) (Consts.extern consts) t'
+  end;
 
 in
 
@@ -487,7 +495,7 @@
 
 (* local abbreviations *)
 
-fun expand_consts ctxt =
+fun certify_consts ctxt =
   Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt);
 
 fun expand_binds ctxt schematic =
@@ -532,7 +540,7 @@
     (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s
       handle TERM (msg, _) => error msg)
     |> app (intern_skolem ctxt internal)
-    |> app (expand_consts ctxt)
+    |> app (certify_consts ctxt)
     |> app (if pattern then I else expand_binds ctxt schematic)
     |> app (if pattern then prepare_dummies else reject_dummies)
   end;
@@ -563,12 +571,14 @@
 
 (* certify terms *)
 
+val test = ref (NONE: (context * term) option);
+
 local
 
 fun gen_cert prop pattern schematic ctxt t = t
-  |> expand_consts ctxt
+  |> certify_consts ctxt
   |> (if pattern then I else expand_binds ctxt schematic)
-  |> (fn t' => #1 (Sign.certify false prop (pp ctxt) (theory_of ctxt) t')
+  |> (fn t' => #1 (Sign.certify' false prop (pp ctxt) (consts_of ctxt) (theory_of ctxt) t')
     handle TYPE (msg, _, _) => error msg
       | TERM (msg, _) => error msg);
 
@@ -1071,8 +1081,7 @@
 fun prep_vars prep_typ internal legacy =
   fold_map (fn (raw_x, raw_T, raw_mx) => fn ctxt =>
     let
-      val x = Syntax.const_name raw_x raw_mx;
-      val mx = Syntax.fix_mixfix raw_x raw_mx;
+      val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
       val _ =
         if not legacy andalso not (Syntax.is_identifier (no_skolem internal x)) then
           error ("Illegal variable name: " ^ quote x)
@@ -1097,13 +1106,19 @@
 
 (* abbreviations *)
 
+val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
+
 local
 
-fun gen_abbrevs prep_vars prep_term revert = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt =>
+fun gen_abbrevs prep_vars prep_term (mode, inout) = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt =>
   let
-    val thy = theory_of ctxt and naming = naming_of ctxt;
+    val thy = theory_of ctxt;
+    val naming = naming_of ctxt
+      |> K (mode <> "") ? (NameSpace.add_path mode #> NameSpace.no_base_names);
+
     val ([(c, _, mx)], _) = prep_vars [(raw_c, NONE, raw_mx)] ctxt;
-    val [t] = polymorphic ctxt [prep_term ctxt raw_t];
+    val (c', b) = Syntax.mixfix_const (NameSpace.full naming c) mx;
+    val [t] = polymorphic ctxt [prep_term (ctxt |> expand_abbrevs false) raw_t];
     val T = Term.fastype_of t;
     val _ =
       if null (hidden_polymorphism t T) then ()
@@ -1111,8 +1126,8 @@
   in
     ctxt
     |> declare_term t
-    |> map_consts (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming revert (c, t)))
-    |> map_syntax (LocalSyntax.add_syntax thy [(false, (NameSpace.full naming c, T, mx))])
+    |> map_consts (apsnd (Consts.abbreviate (pp ctxt) (tsig_of ctxt) naming mode ((c, t), b)))
+    |> map_syntax (LocalSyntax.add_syntax thy (mode, inout) [(false, (c', T, mx))])
   end);
 
 in
@@ -1138,6 +1153,8 @@
 
 fun gen_fixes prep raw_vars ctxt =
   let
+    val thy = theory_of ctxt;
+
     val (ys, zs) = split_list (fixes_of ctxt);
     val (vars, ctxt') = prep raw_vars ctxt;
     val xs = map #1 vars;
@@ -1149,7 +1166,7 @@
     ctxt'
     |> map_fixes (fn (b, fixes) => (b, rev (xs ~~ xs') @ fixes))
     |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
-    |-> (map_syntax o LocalSyntax.add_syntax (theory_of ctxt) o map prep_mixfix)
+    |-> (map_syntax o LocalSyntax.add_syntax thy Syntax.default_mode o map prep_mixfix)
     |> pair xs'
   end;