merged

--- a/src/Pure/General/name_space.ML	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 25 14:07:59 2013 +0100
@@ -31,6 +31,8 @@
   val names_unique_raw: Config.raw
   val names_unique: bool Config.T
   val extern: Proof.context -> T -> string -> xstring
+  val extern_ord: Proof.context -> T -> string * string -> order
+  val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
@@ -194,6 +196,10 @@
     else ext (get_accesses space name)
   end;
 
+fun extern_ord ctxt space = string_ord o pairself (extern ctxt space);
+
+fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
+
 
 (* modify internals *)
 

--- a/src/Pure/General/pretty.ML	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Pure/General/pretty.ML	Mon Mar 25 14:07:59 2013 +0100
@@ -168,7 +168,12 @@
 val chunks = markup_chunks Markup.empty;
 
 fun chunks2 prts =
-  blk (0, flat (Library.separate [fbrk, fbrk] (map (single o mark Markup.text_fold) prts)));
+  (case try split_last prts of
+    NONE => blk (0, [])
+  | SOME (prefix, last) =>
+      blk (0,
+        maps (fn prt => [markup Markup.text_fold [prt, fbrk], fbrk]) prefix @
+        [mark Markup.text_fold last]));
 
 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
 

--- a/src/Pure/General/pretty.scala	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Pure/General/pretty.scala	Mon Mar 25 14:07:59 2013 +0100
@@ -31,14 +31,12 @@
   abstract class Metric
   {
     val unit: Double
-    def average: Double
     def apply(s: String): Double
   }
 
   object Metric_Default extends Metric
   {
     val unit = 1.0
-    val average = 1.0
     def apply(s: String): Double = s.length.toDouble
   }
 

--- a/src/Pure/Isar/class.ML	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Pure/Isar/class.ML	Mon Mar 25 14:07:59 2013 +0100
@@ -161,34 +161,50 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
+
+    val class_space = Proof_Context.class_space ctxt;
+    val type_space = Proof_Context.type_space ctxt;
+    val const_space = Proof_Context.const_space ctxt;
+
     val arities =
       Symtab.empty
       |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
            Symtab.map_default (class, []) (insert (op =) tyco)) arities)
              (Sorts.arities_of algebra);
-    val the_arities = these o Symtab.lookup arities;
-    fun mk_arity class tyco =
+
+    fun prt_supersort class =
+      Syntax.pretty_sort ctxt (Sign.minimize_sort thy (Sign.super_classes thy class));
+
+    fun prt_arity class tyco =
       let
         val Ss = Sorts.mg_domain algebra tyco [class];
       in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
-    fun mk_param (c, ty) =
-      Pretty.str (Proof_Context.extern_const ctxt c ^ " :: " ^
-        Syntax.string_of_typ ctxt (Type.strip_sorts_dummy ty));
-    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
-      (SOME o Pretty.str) ("class " ^ Proof_Context.extern_class ctxt class ^ ":"),
-      (SOME o Pretty.block) [Pretty.str "supersort: ",
-        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
-      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
-          (Pretty.str "parameters:" :: ps)) o map mk_param
-        o these o Option.map #params o try (AxClass.get_info thy)) class,
-      (SOME o Pretty.block o Pretty.breaks) [
-        Pretty.str "instances:",
-        Pretty.list "" "" (map (mk_arity class) (the_arities class))
-      ]
-    ]
+
+    fun prt_param (c, ty) =
+      Pretty.block
+       [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::",
+        Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
+
+    fun prt_entry class =
+      Pretty.block
+        ([Pretty.command "class", Pretty.brk 1,
+          Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
+          Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
+          (case try (AxClass.get_info thy) class of
+            NONE => []
+          | SOME {params, ...} =>
+              [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
+          (case Symtab.lookup arities class of
+            NONE => []
+          | SOME ars =>
+              [Pretty.fbrk, Pretty.big_list "instances:"
+                (map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))]));
   in
-    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
-      o map mk_entry o Sorts.all_classes) algebra
+    Sorts.all_classes algebra
+    |> sort (Name_Space.extern_ord ctxt class_space)
+    |> map prt_entry
+    |> Pretty.chunks2
+    |> Pretty.writeln
   end;
 
 

--- a/src/Pure/build-jars	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Pure/build-jars	Mon Mar 25 14:07:59 2013 +0100
@@ -211,7 +211,7 @@
       isabelle_scala scalac $SCALAC_OPTIONS "${PIDE_SOURCES[@]}" "${PURE_SOURCES[@]}" || \
         fail "Failed to compile sources"
     fi
-  )
+  ) || exit "$?"
 
   mkdir -p "$TARGET_DIR/ext" || fail "Failed to create directory $TARGET_DIR/ext"
 

--- a/src/Pure/display.ML	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Pure/display.ML	Mon Mar 25 14:07:59 2013 +0100
@@ -122,8 +122,7 @@
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
-          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 ::
-            Pretty.commas (map prt_cls cs));
+          (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
 
     fun pretty_default S = Pretty.block
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
@@ -171,7 +170,8 @@
     val arities = Sorts.arities_of class_algebra;
 
     val clsses =
-      Name_Space.dest_table ctxt (class_space, Symtab.make (map (apfst fst) (Graph.dest classes)));
+      Name_Space.dest_table ctxt (class_space,
+        Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)));
     val tdecls = Name_Space.dest_table ctxt types;
     val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
 

--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Mar 25 13:50:50 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Mar 25 14:07:59 2013 +0100
@@ -168,7 +168,7 @@
   // NB: last line lacks \n
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {
-    val metric = JEdit_Lib.pretty_metric(text_area.getPainter)
+    val metric = pretty_metric(text_area.getPainter)
     val char_width = (metric.unit * metric.average).round.toInt
 
     val buffer = text_area.getBuffer
@@ -208,14 +208,19 @@
 
   /* pretty text metric */
 
-  def string_width(painter: TextAreaPainter, s: String): Double =
-    painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
+  abstract class Pretty_Metric extends Pretty.Metric
+  {
+    def average: Double
+  }
 
-  def pretty_metric(painter: TextAreaPainter): Pretty.Metric =
-    new Pretty.Metric {
-      val unit = string_width(painter, Pretty.space)
-      val average = string_width(painter, "mix") / (3 * unit)
-      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(painter, s) / unit
+  def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
+    new Pretty_Metric {
+      def string_width(s: String): Double =
+        painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
+
+      val unit = string_width(Pretty.space)
+      val average = string_width("mix") / (3 * unit)
+      def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }
 }