# HG changeset patch
# User wenzelm
# Date 1273342451 -7200
# Node ID 275b24cf9c4122bd50b4dcd7485f3192f27e84ef
# Parent  21443c2858a73deab4b494f2860a3da9d72fddee# Parent  5548f749191e68613cd1113df26127baca55767f
merged

diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat May 08 20:14:11 2010 +0200
@@ -212,8 +212,7 @@
 
 text {*
   \begin{mldecls}
-    @{index_ML Pretty.setdepth: "int -> unit"} \\
-    @{index_ML Pretty.setmargin: "int -> unit"} \\
+    @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
     @{index_ML print_depth: "int -> unit"} \\
   \end{mldecls}
 
@@ -221,16 +220,12 @@
 
   \begin{description}
 
-  \item @{ML Pretty.setdepth}~@{text d} tells the pretty printer to
-  limit the printing depth to @{text d}.  This affects the display of
-  types, terms, theorems etc.  The default value is 0, which permits
-  printing to an arbitrary depth.  Other useful values for @{text d}
-  are 10 and 20.
-
-  \item @{ML Pretty.setmargin}~@{text m} tells the pretty printer to
-  assume a right margin (page width) of @{text m}.  The initial margin
-  is 76, but user interfaces might adapt the margin automatically when
-  resizing windows.
+  \item @{ML Pretty.margin_default} indicates the global default for
+  the right margin of the built-in pretty printer, with initial value
+  76.  Note that user-interfaces typically control margins
+  automatically when resizing windows, or even bypass the formatting
+  engine of Isabelle/ML altogether and do it within the front end via
+  Isabelle/Scala.
 
   \item @{ML print_depth}~@{text n} limits the printing depth of the
   ML toplevel pretty printer; the precise effect depends on the ML
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat May 08 20:14:11 2010 +0200
@@ -231,8 +231,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-    \indexdef{}{ML}{Pretty.setdepth}\verb|Pretty.setdepth: int -> unit| \\
-    \indexdef{}{ML}{Pretty.setmargin}\verb|Pretty.setmargin: int -> unit| \\
+    \indexdef{}{ML}{Pretty.margin\_default}\verb|Pretty.margin_default: int Unsynchronized.ref| \\
     \indexdef{}{ML}{print\_depth}\verb|print_depth: int -> unit| \\
   \end{mldecls}
 
@@ -240,16 +239,12 @@
 
   \begin{description}
 
-  \item \verb|Pretty.setdepth|~\isa{d} tells the pretty printer to
-  limit the printing depth to \isa{d}.  This affects the display of
-  types, terms, theorems etc.  The default value is 0, which permits
-  printing to an arbitrary depth.  Other useful values for \isa{d}
-  are 10 and 20.
-
-  \item \verb|Pretty.setmargin|~\isa{m} tells the pretty printer to
-  assume a right margin (page width) of \isa{m}.  The initial margin
-  is 76, but user interfaces might adapt the margin automatically when
-  resizing windows.
+  \item \verb|Pretty.margin_default| indicates the global default for
+  the right margin of the built-in pretty printer, with initial value
+  76.  Note that user-interfaces typically control margins
+  automatically when resizing windows, or even bypass the formatting
+  engine of Isabelle/ML altogether and do it within the front end via
+  Isabelle/Scala.
 
   \item \verb|print_depth|~\isa{n} limits the printing depth of the
   ML toplevel pretty printer; the precise effect depends on the ML
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Sat May 08 20:14:11 2010 +0200
@@ -9,7 +9,7 @@
   "gcd m n = (if n=0 then m else gcd n (m mod n))"
 
 
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
 ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
 
 
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Sat May 08 20:14:11 2010 +0200
@@ -2,7 +2,7 @@
 theory Examples imports Main Binomial begin
 
 ML "Unsynchronized.reset eta_contract"
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
 
 text{*membership, intersection *}
 text{*difference and empty set*}
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Sets/Functions.thy
--- a/doc-src/TutorialI/Sets/Functions.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy	Sat May 08 20:14:11 2010 +0200
@@ -1,7 +1,7 @@
 (* ID:         $Id$ *)
 theory Functions imports Main begin
 
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
 
 
 text{*
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Sets/Recur.thy
--- a/doc-src/TutorialI/Sets/Recur.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Recur.thy	Sat May 08 20:14:11 2010 +0200
@@ -1,7 +1,7 @@
 (* ID:         $Id$ *)
 theory Recur imports Main begin
 
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
 
 
 text{*
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy	Sat May 08 20:14:11 2010 +0200
@@ -1,7 +1,7 @@
 (* ID:         $Id$ *)
 theory Relations imports Main begin
 
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
 
 (*Id is only used in UNITY*)
 (*refl, antisym,trans,univalent,\<dots> ho hum*)
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Sat May 08 20:14:11 2010 +0200
@@ -2,7 +2,7 @@
 imports Complex_Main
 begin
 
-ML "Pretty.setmargin 64"
+ML "Pretty.margin_default := 64"
 ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)
 
 text{*
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/TutorialI/Types/document/Numbers.tex
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Sat May 08 20:14:11 2010 +0200
@@ -26,7 +26,7 @@
 %
 \isatagML
 \isacommand{ML}\isamarkupfalse%
-\ {\isachardoublequoteopen}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
 \isacommand{ML}\isamarkupfalse%
 \ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
 \endisatagML
diff -r 21443c2858a7 -r 275b24cf9c41 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Sat May 08 20:01:28 2010 +0200
+++ b/doc-src/more_antiquote.ML	Sat May 08 20:14:11 2010 +0200
@@ -51,7 +51,7 @@
 
 local
 
-val pr_text = enclose "\\isa{" "}" o Pretty.output o Pretty.str;
+val pr_text = enclose "\\isa{" "}" o Pretty.output NONE o Pretty.str;
 
 fun pr_class ctxt = ProofContext.read_class ctxt
   #> Type.extern_class (ProofContext.tsig_of ctxt)
diff -r 21443c2858a7 -r 275b24cf9c41 src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sat May 08 20:14:11 2010 +0200
@@ -13,7 +13,7 @@
 fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
   let
     val thms = Mirabelle.theorems_of_sucessful_proof post
-    val names = map Thm.get_name thms
+    val names = map Thm.get_name_hint thms
     val add_info = if null names then I else suffix (":\n" ^ commas names)
 
     val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
diff -r 21443c2858a7 -r 275b24cf9c41 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sat May 08 20:14:11 2010 +0200
@@ -648,7 +648,7 @@
        val mutated = mutate option (prop_of x) usedthy
          commutatives forbidden_funs iter
        val (passednum,_,cenum,_) = qc_test mutated insts usedthy sz qciter
-       val thmname =  "\ntheorem " ^ (Thm.get_name x) ^ ":"
+       val thmname =  "\ntheorem " ^ Thm.get_name_hint x ^ ":"
        val pnumstring = string_of_int passednum
        val cenumstring = string_of_int cenum
      in
diff -r 21443c2858a7 -r 275b24cf9c41 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sat May 08 20:14:11 2010 +0200
@@ -302,7 +302,7 @@
   end
 
 fun create_entry thy thm exec mutants mtds =
-  (Thm.get_name thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
+  (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
 *)
 fun create_detailed_entry thy thm exec mutants mtds =
   let
@@ -310,7 +310,7 @@
       map (fn (mtd_name, invoke_mtd) =>
         (mtd_name, safe_invoke_mtd thy (mtd_name, invoke_mtd) mutant)) mtds)
   in
-    (Thm.get_name thm, exec, prop_of thm, map create_mutant_subentry mutants)
+    (Thm.get_name_hint thm, exec, prop_of thm, map create_mutant_subentry mutants)
   end
 
 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
diff -r 21443c2858a7 -r 275b24cf9c41 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat May 08 20:14:11 2010 +0200
@@ -120,7 +120,7 @@
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
 
-    val ind_name = Thm.get_name induct;
+    val ind_name = Thm.derivation_name induct;
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
       |> Sign.root_path
@@ -191,7 +191,7 @@
             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
 
-    val exh_name = Thm.get_name exhaust;
+    val exh_name = Thm.derivation_name exhaust;
     val (thm', thy') = thy
       |> Sign.root_path
       |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm)
diff -r 21443c2858a7 -r 275b24cf9c41 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 08 20:14:11 2010 +0200
@@ -408,7 +408,7 @@
       in
         Extraction.add_realizers_i
           (map (fn (((ind, corr), rlz), r) =>
-              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
+              mk_realizer thy' (vs' @ Ps) (Thm.derivation_name ind, ind, corr, rlz, r))
             realizers @ (case realizers of
              [(((ind, corr), rlz), r)] =>
                [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/General/pretty.ML	Sat May 08 20:14:11 2010 +0200
@@ -52,17 +52,16 @@
   val big_list: string -> T list -> T
   val indent: int -> T -> T
   val unbreakable: T -> T
-  val setmargin: int -> unit
-  val setmp_margin_CRITICAL: int -> ('a -> 'b) -> 'a -> 'b
-  val setdepth: int -> unit
-  val to_ML: T -> ML_Pretty.pretty
-  val from_ML: ML_Pretty.pretty -> T
+  val margin_default: int Unsynchronized.ref
   val symbolicN: string
-  val output_buffer: T -> Buffer.T
-  val output: T -> output
+  val output_buffer: int option -> T -> Buffer.T
+  val output: int option -> T -> output
+  val string_of_margin: int -> T -> string
   val string_of: T -> string
   val str_of: T -> string
   val writeln: T -> unit
+  val to_ML: T -> ML_Pretty.pretty
+  val from_ML: ML_Pretty.pretty -> T
   type pp
   val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
   val term: pp -> term -> T
@@ -179,34 +178,6 @@
 
 (** formatting **)
 
-(* margin *)
-
-fun make_margin_info m =
- {margin = m,                   (*right margin, or page width*)
-  breakgain = m div 20,         (*minimum added space required of a break*)
-  emergencypos = m div 2};      (*position too far to right*)
-
-val margin_info = Unsynchronized.ref (make_margin_info 76);
-fun setmargin m = margin_info := make_margin_info m;
-fun setmp_margin_CRITICAL m f = setmp_CRITICAL margin_info (make_margin_info m) f;
-
-
-(* depth limitation *)
-
-val depth = Unsynchronized.ref 0;   (*maximum depth; 0 means no limit*)
-fun setdepth dp = (depth := dp);
-
-local
-  fun pruning dp (Block (m, bes, indent, _)) =
-        if dp > 0
-        then block_markup m (indent, map (pruning (dp - 1)) bes)
-        else str "..."
-    | pruning _ e = e;
-in
-  fun prune e = if ! depth > 0 then pruning (! depth) e else e;
-end;
-
-
 (* formatted output *)
 
 local
@@ -259,42 +230,45 @@
   | forcenext (Break _ :: es) = fbrk :: es
   | forcenext (e :: es) = e :: forcenext es;
 
-(*es is list of expressions to print;
-  blockin is the indentation of the current block;
-  after is the width of the following context until next break.*)
-fun format ([], _, _) text = text
-  | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
-      (case e of
-        Block ((bg, en), bes, indent, _) =>
-          let
-            val {emergencypos, ...} = ! margin_info;
-            val pos' = pos + indent;
-            val pos'' = pos' mod emergencypos;
-            val block' =
-              if pos' < emergencypos then (ind |> add_indent indent, pos')
-              else (add_indent pos'' Buffer.empty, pos'');
-            val btext: text = text
-              |> control bg
-              |> format (bes, block', breakdist (es, after))
-              |> control en;
-            (*if this block was broken then force the next break*)
-            val es' = if nl < #nl btext then forcenext es else es;
-          in format (es', block, after) btext end
-      | Break (force, wd) =>
-          let val {margin, breakgain, ...} = ! margin_info in
-            (*no break if text to next break fits on this line
-              or if breaking would add only breakgain to space*)
-            format (es, block, after)
-              (if not force andalso
-                  pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
-                then text |> blanks wd  (*just insert wd blanks*)
-                else text |> newline |> indentation block)
-          end
-      | String str => format (es, block, after) (string str text));
-
 in
 
-fun formatted e = #tx (format ([prune e], (Buffer.empty, 0), 0) empty);
+fun formatted margin input =
+  let
+    val breakgain = margin div 20;     (*minimum added space required of a break*)
+    val emergencypos = margin div 2;   (*position too far to right*)
+
+    (*es is list of expressions to print;
+      blockin is the indentation of the current block;
+      after is the width of the following context until next break.*)
+    fun format ([], _, _) text = text
+      | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
+          (case e of
+            Block ((bg, en), bes, indent, _) =>
+              let
+                val pos' = pos + indent;
+                val pos'' = pos' mod emergencypos;
+                val block' =
+                  if pos' < emergencypos then (ind |> add_indent indent, pos')
+                  else (add_indent pos'' Buffer.empty, pos'');
+                val btext: text = text
+                  |> control bg
+                  |> format (bes, block', breakdist (es, after))
+                  |> control en;
+                (*if this block was broken then force the next break*)
+                val es' = if nl < #nl btext then forcenext es else es;
+              in format (es', block, after) btext end
+          | Break (force, wd) =>
+              (*no break if text to next break fits on this line
+                or if breaking would add only breakgain to space*)
+              format (es, block, after)
+                (if not force andalso
+                    pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
+                  then text |> blanks wd  (*just insert wd blanks*)
+                  else text |> newline |> indentation block)
+          | String str => format (es, block, after) (string str text));
+  in
+    #tx (format ([input], (Buffer.empty, 0), 0) empty)
+  end;
 
 end;
 
@@ -318,10 +292,28 @@
     fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
       | fmt (String (s, _)) = Buffer.add s
       | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
-  in fmt (prune prt) Buffer.empty end;
+  in fmt prt Buffer.empty end;
 
 
-(* ML toplevel pretty printing *)
+(* output interfaces *)
+
+val margin_default = Unsynchronized.ref 76;  (*right margin, or page width*)
+
+val symbolicN = "pretty_symbolic";
+
+fun output_buffer margin prt =
+  if print_mode_active symbolicN then symbolic prt
+  else formatted (the_default (! margin_default) margin) prt;
+
+val output = Buffer.content oo output_buffer;
+fun string_of_margin margin = Output.escape o output (SOME margin);
+val string_of = Output.escape o output NONE;
+val str_of = Output.escape o Buffer.content o unformatted;
+val writeln = Output.writeln o string_of;
+
+
+
+(** ML toplevel pretty printing **)
 
 fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   | to_ML (String s) = ML_Pretty.String s
@@ -332,20 +324,6 @@
   | from_ML (ML_Pretty.Break b) = Break b;
 
 
-(* output interfaces *)
-
-val symbolicN = "pretty_symbolic";
-
-fun output_buffer prt =
-  if print_mode_active symbolicN then symbolic prt
-  else formatted prt;
-
-val output = Buffer.content o output_buffer;
-val string_of = Output.escape o output;
-val str_of = Output.escape o Buffer.content o unformatted;
-val writeln = Output.writeln o string_of;
-
-
 
 (** abstract pretty printing context **)
 
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sat May 08 20:14:11 2010 +0200
@@ -78,9 +78,9 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  private val default_margin = 76
+  private val margin_default = 76
 
-  def formatted(input: List[XML.Tree], margin: Int = default_margin): List[XML.Tree] =
+  def formatted(input: List[XML.Tree], margin: Int = margin_default): List[XML.Tree] =
   {
     val breakgain = margin / 20
     val emergencypos = margin / 2
@@ -115,7 +115,7 @@
     format(input.flatMap(standard_format), 0, 0, Text()).content
   }
 
-  def string_of(input: List[XML.Tree], margin: Int = default_margin): String =
+  def string_of(input: List[XML.Tree], margin: Int = margin_default): String =
     formatted(input).iterator.flatMap(XML.content).mkString
 
 
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Isar/class.ML	Sat May 08 20:14:11 2010 +0200
@@ -202,7 +202,7 @@
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs = if null vs
       then error ("No type variable in part of specification element "
-        ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
+        ^ (Pretty.string_of o Pretty.chunks) (Element.pretty_ctxt class_ctxt e))
       else ();
     fun check_element (e as Element.Fixes fxs) =
           map (fn (_, SOME T, _) => check_vars e (Term.add_tfreesT T [])) fxs
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat May 08 20:14:11 2010 +0200
@@ -313,7 +313,7 @@
 
 (* pretty_setmargin *)
 
-fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
+fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
 
 
 (* print parts of theory and proof context *)
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Sat May 08 20:14:11 2010 +0200
@@ -303,7 +303,7 @@
     val rd = Proof_Syntax.read_proof thy' false;
   in fn (thm, (vs, s1, s2)) =>
     let
-      val name = Thm.get_name thm;
+      val name = Thm.derivation_name thm;
       val _ = name <> "" orelse error "add_realizers: unnamed theorem";
       val prop = Pattern.rewrite_term thy'
         (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
@@ -348,7 +348,7 @@
     val {realizes_eqns, typeof_eqns, types, realizers,
       defs, expand, prep} = ExtractionData.get thy;
 
-    val name = Thm.get_name thm;
+    val name = Thm.derivation_name thm;
     val _ = name <> "" orelse error "add_expand_thm: unnamed theorem";
   in
     thy |> ExtractionData.put
@@ -706,7 +706,7 @@
         val thy = Thm.theory_of_thm thm;
         val prop = Thm.prop_of thm;
         val prf = Thm.proof_of thm;
-        val name = Thm.get_name thm;
+        val name = Thm.derivation_name thm;
         val _ = name <> "" orelse error "extraction: unnamed theorem";
         val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
           quote name ^ " has no computational content")
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sat May 08 20:14:11 2010 +0200
@@ -244,7 +244,7 @@
 fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
-    val defnames = map Thm.get_name defs;
+    val defnames = map Thm.derivation_name defs;
     val f = if not r then I else
       let
         val cnames = map (fst o dest_Const o fst) defs';
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat May 08 20:14:11 2010 +0200
@@ -698,21 +698,23 @@
   in (syms, pos) end;
 
 local
-  type operations =
-   {parse_sort: Proof.context -> string -> sort,
-    parse_typ: Proof.context -> string -> typ,
-    parse_term: Proof.context -> string -> term,
-    parse_prop: Proof.context -> string -> term,
-    unparse_sort: Proof.context -> sort -> Pretty.T,
-    unparse_typ: Proof.context -> typ -> Pretty.T,
-    unparse_term: Proof.context -> term -> Pretty.T};
 
-  val operations = Unsynchronized.ref (NONE: operations option);
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+  parse_typ: Proof.context -> string -> typ,
+  parse_term: Proof.context -> string -> term,
+  parse_prop: Proof.context -> string -> term,
+  unparse_sort: Proof.context -> sort -> Pretty.T,
+  unparse_typ: Proof.context -> typ -> Pretty.T,
+  unparse_term: Proof.context -> term -> Pretty.T};
 
-  fun operation which ctxt x =
-    (case ! operations of
-      NONE => error "Inner syntax operations not yet installed"
-    | SOME ops => which ops ctxt x);
+val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
+
+fun operation which ctxt x =
+  (case Single_Assignment.peek operations of
+    NONE => raise Fail "Inner syntax operations not installed"
+  | SOME ops => which ops ctxt x);
+
 in
 
 val parse_sort = operation #parse_sort;
@@ -723,9 +725,7 @@
 val unparse_typ = operation #unparse_typ;
 val unparse_term = operation #unparse_term;
 
-fun install_operations ops = CRITICAL (fn () =>
-  if is_some (! operations) then error "Inner syntax operations already installed"
-  else operations := SOME ops);
+fun install_operations ops = Single_Assignment.assign operations ops;
 
 end;
 
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat May 08 20:14:11 2010 +0200
@@ -53,7 +53,7 @@
       else
         let val {concealed, group, ...} = Name_Space.the_entry space name in
           fold_rev (fn th =>
-            (case Thm.get_name th of
+            (case Thm.derivation_name th of
               "" => I
             | a => cons (a, (th, concealed, group)))) ths
         end;
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat May 08 20:14:11 2010 +0200
@@ -428,7 +428,7 @@
   ("break", setmp_CRITICAL break o boolean),
   ("quotes", setmp_CRITICAL quotes o boolean),
   ("mode", fn s => fn f => PrintMode.with_modes [s] f),
-  ("margin", Pretty.setmp_margin_CRITICAL o integer),
+  ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   ("indent", setmp_CRITICAL indent o integer),
   ("source", setmp_CRITICAL source o boolean),
   ("goals_limit", setmp_CRITICAL goals_limit o integer)];
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/axclass.ML	Sat May 08 20:14:11 2010 +0200
@@ -241,7 +241,7 @@
   end;
 
 
-fun the_arity thy a (c, Ss) =
+fun the_arity thy (a, Ss, c) =
   (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
     SOME (thm, _) => Thm.transfer thy thm
   | NONE => error ("Unproven type arity " ^
@@ -295,10 +295,12 @@
   end;
 
 val _ = Context.>> (Context.map_theory
-  (Theory.at_begin complete_classrels #> Theory.at_begin complete_arities));
+  (Theory.at_begin complete_classrels #>
+   Theory.at_begin complete_arities));
 
-val the_classrel_prf = Thm.proof_of oo the_classrel;
-val the_arity_prf = Thm.proof_of ooo the_arity;
+val _ = Proofterm.install_axclass_proofs
+  {classrel_proof = Thm.proof_of oo the_classrel,
+   arity_proof = Thm.proof_of oo the_arity};
 
 
 (* maintain instance parameters *)
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/codegen.ML	Sat May 08 20:14:11 2010 +0200
@@ -109,9 +109,7 @@
 
 val margin = Unsynchronized.ref 80;
 
-fun string_of p = (Pretty.string_of |>
-  PrintMode.setmp [] |>
-  Pretty.setmp_margin_CRITICAL (!margin)) p;
+fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
 
 val str = PrintMode.setmp [] Pretty.str;
 
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/more_thm.ML	Sat May 08 20:14:11 2010 +0200
@@ -326,7 +326,7 @@
 (* close_derivation *)
 
 fun close_derivation thm =
-  if Thm.get_name thm = "" then Thm.put_name "" thm
+  if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
   else thm;
 
 
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/proofterm.ML	Sat May 08 20:14:11 2010 +0200
@@ -84,7 +84,7 @@
   val varify_proof: term -> (string * sort) list -> proof -> proof
   val legacy_freezeT: term -> proof -> proof
   val rotate_proof: term list -> term -> int -> proof -> proof
-  val permute_prems_prf: term list -> int -> int -> proof -> proof
+  val permute_prems_proof: term list -> int -> int -> proof -> proof
   val generalize: string list * string list -> int -> proof -> proof
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     -> proof -> proof
@@ -110,6 +110,12 @@
   val equal_elim: term -> term -> proof -> proof -> proof
   val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
     sort list -> proof -> proof
+  val classrel_proof: theory -> class * class -> proof
+  val arity_proof: theory -> string * sort list * class -> proof
+  val of_sort_proof: theory -> (typ * class -> proof) -> typ * sort -> proof list
+  val install_axclass_proofs:
+   {classrel_proof: theory -> class * class -> proof,
+    arity_proof: theory -> string * sort list * class -> proof} -> unit
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
   val promise_proof: theory -> serial -> term -> proof
@@ -689,7 +695,7 @@
 
 (***** permute premises *****)
 
-fun permute_prems_prf prems j k prf =
+fun permute_prems_proof prems j k prf =
   let val n = length prems
   in mk_AbsP (n, proof_combP (prf,
     map PBound ((n-1 downto n-j) @ (k-1 downto 0) @ (n-j-1 downto k))))
@@ -886,7 +892,7 @@
   equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
 
 
-(**** sort hypotheses ****)
+(**** type classes ****)
 
 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
   let
@@ -902,6 +908,53 @@
   in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end;
 
 
+local
+
+type axclass_proofs =
+ {classrel_proof: theory -> class * class -> proof,
+  arity_proof: theory -> string * sort list * class -> proof};
+
+val axclass_proofs: axclass_proofs Single_Assignment.var =
+  Single_Assignment.var "Proofterm.axclass_proofs";
+
+fun axclass_proof which thy x =
+  (case Single_Assignment.peek axclass_proofs of
+    NONE => raise Fail "Axclass proof operations not installed"
+  | SOME prfs => which prfs thy x);
+
+in
+
+val classrel_proof = axclass_proof #classrel_proof;
+val arity_proof = axclass_proof #arity_proof;
+
+fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs;
+
+end;
+
+
+local
+
+fun canonical_instance typs =
+  let
+    val names = Name.invents Name.context Name.aT (length typs);
+    val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs;
+  in instantiate (instT, []) end;
+
+in
+
+fun of_sort_proof thy hyps =
+  Sorts.of_sort_derivation (Sign.classes_of thy)
+   {class_relation = fn typ => fn (prf, c1) => fn c2 =>
+      if c1 = c2 then prf
+      else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf,
+    type_constructor = fn (a, typs) => fn dom => fn c =>
+      let val Ss = map (map snd) dom and prfs = maps (map fst) dom
+      in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end,
+    type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)};
+
+end;
+
+
 (***** axioms and theorems *****)
 
 val proofs = Unsynchronized.ref 2;
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/pure_thy.ML	Sat May 08 20:14:11 2010 +0200
@@ -121,7 +121,7 @@
   | name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs;
 
 fun name_thm pre official name thm = thm
-  |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
+  |> not (Thm.derivation_name thm <> "" andalso pre orelse not official) ? Thm.name_derivation name
   |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name);
 
 fun name_thms pre official name xs =
diff -r 21443c2858a7 -r 275b24cf9c41 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Pure/thm.ML	Sat May 08 20:14:11 2010 +0200
@@ -126,8 +126,8 @@
   val proof_of: thm -> proof
   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
-  val get_name: thm -> string
-  val put_name: string -> thm -> thm
+  val derivation_name: thm -> string
+  val name_derivation: string -> thm -> thm
   val axiom: theory -> string -> thm
   val axioms_of: theory -> (string * thm) list
   val get_tags: thm -> Properties.T
@@ -585,10 +585,10 @@
 
 (* closed derivations with official name *)
 
-fun get_name thm =
+fun derivation_name thm =
   Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
 
-fun put_name name (thm as Thm (der, args)) =
+fun name_derivation name (thm as Thm (der, args)) =
   let
     val Deriv {promises, body} = der;
     val {thy_ref, hyps, prop, tpairs, ...} = args;
@@ -1436,7 +1436,7 @@
         in Logic.list_implies (fixed_prems @ qs @ ps, concl) end
       else raise THM ("permute_prems: k", k, [rl]);
   in
-    Thm (deriv_rule1 (Pt.permute_prems_prf prems j m) der,
+    Thm (deriv_rule1 (Pt.permute_prems_proof prems j m) der,
      {thy_ref = thy_ref,
       tags = [],
       maxidx = maxidx,
diff -r 21443c2858a7 -r 275b24cf9c41 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Sat May 08 20:14:11 2010 +0200
@@ -116,8 +116,8 @@
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
 fun indent i = PrintMode.setmp [] (Pretty.indent i);
 
-fun string_of_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.string_of) p ^ "\n";
-fun writeln_pretty width p = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL width Pretty.writeln) p;
+fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
+fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
 
 
 (** names and variable name contexts **)
diff -r 21443c2858a7 -r 275b24cf9c41 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Sat May 08 20:01:28 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Sat May 08 20:14:11 2010 +0200
@@ -143,7 +143,7 @@
 fun html_thm ctxt (n, (thmref, thm)) =
   let
     val string_of_thm =
-      Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
+      Output.output o Pretty.string_of_margin 100 o
         setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
   in
     tag' "tr" (class ("row" ^ Int.toString (n mod 2)))