# HG changeset patch
# User wenzelm
# Date 1144529486 -7200
# Node ID b048aa441c3413a6a0c190d1d288d9f86e3d49b8
# Parent  a4374b41c9bf29fec0d49b43fe65c27d6fa31800
abbrevs: support print mode;

diff -r a4374b41c9bf -r b048aa441c34 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Apr 08 22:51:25 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Apr 08 22:51:26 2006 +0200
@@ -41,7 +41,7 @@
   val def_finish: (local_theory -> term -> thm -> thm) ->
     (bstring * mixfix) * ((bstring * Attrib.src list) * term) ->
     local_theory -> (term * (bstring * thm)) * local_theory
-  val abbrev: bool -> (bstring * mixfix) * term -> local_theory -> local_theory
+  val abbrev: string * bool -> (bstring * mixfix) * term -> local_theory -> local_theory
 end;
 
 structure LocalTheory: LOCAL_THEORY =
@@ -181,8 +181,8 @@
       NONE => theory (Sign.add_consts_i (map (fn ((c, T), mx) => (c, T, mx)) decls))
     | SOME (loc, _) =>
         theory (Sign.add_consts_i (map (fn ((c, T), _) => (c, Ps ---> T, NoSyn)) decls)) #>
-        locale (Locale.add_abbrevs loc true abbrevs) #>
-        ProofContext.add_abbrevs_i true abbrevs)
+        locale (Locale.add_abbrevs loc Syntax.default_mode abbrevs) #>
+        ProofContext.add_abbrevs_i Syntax.default_mode abbrevs)
     |> pair (map #2 abbrevs)
   end;
 
@@ -280,15 +280,15 @@
 
 (* constant abbreviations *)
 
-fun abbrev revert ((x, mx), rhs) ctxt =
+fun abbrev prmode ((x, mx), rhs) ctxt =
   let val abbrevs = [(x, rhs, mx)] in
     ctxt |>
     (case locale_of ctxt of
       NONE =>
-        theory (Sign.add_abbrevs_i revert abbrevs)
+        theory (Sign.add_abbrevs_i prmode abbrevs)
     | SOME (loc, _) =>
-        locale (Locale.add_abbrevs loc revert abbrevs) #>
-        ProofContext.add_abbrevs_i revert abbrevs)
+        locale (Locale.add_abbrevs loc prmode abbrevs) #>
+        ProofContext.add_abbrevs_i prmode abbrevs)
   end;
 
 end;
diff -r a4374b41c9bf -r b048aa441c34 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Apr 08 22:51:25 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Apr 08 22:51:26 2006 +0200
@@ -87,7 +87,7 @@
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     cterm list * Proof.context ->
     ((string * thm list) list * (string * thm list) list) * Proof.context
-  val add_abbrevs: string -> bool -> (bstring * term * mixfix) list ->
+  val add_abbrevs: string -> string * bool -> (bstring * term * mixfix) list ->
     cterm list * Proof.context -> Proof.context
 
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
@@ -150,7 +150,7 @@
   elems: (Element.context_i * stamp) list,                          (*static content*)
   params: ((string * typ) * mixfix) list,                           (*all params*)
   lparams: string list,                                             (*local parmas*)
-  abbrevs: ((bool * (bstring * term * mixfix) list) * stamp) list,  (*abbreviations*)
+  abbrevs: (((string * bool) * (bstring * term * mixfix) list) * stamp) list,  (*abbreviations*)
   regs: ((string * string list) * (term * thm) list) list}
     (* Registrations: indentifiers and witness theorems of locales interpreted
        in the locale.
@@ -1490,11 +1490,11 @@
 
 (* abbreviations *)
 
-fun add_abbrevs loc revert decls =
-  snd #> ProofContext.add_abbrevs_i revert decls #>
+fun add_abbrevs loc prmode decls =
+  snd #> ProofContext.add_abbrevs_i prmode decls #>
   ProofContext.map_theory (change_locale loc
     (fn (predicate, import, elems, params, lparams, abbrevs, regs) =>
-      (predicate, import, elems, params, lparams, ((revert, decls), stamp ()) :: abbrevs, regs)));
+      (predicate, import, elems, params, lparams, ((prmode, decls), stamp ()) :: abbrevs, regs)));
 
 fun init_abbrevs loc ctxt =
   fold_rev (uncurry ProofContext.add_abbrevs_i o fst)