# HG changeset patch
# User huffman
# Date 1274571978 25200
# Node ID 3a7c2c949320aa8119cb984dbf74e13de10e0aa0
# Parent  b2073920448f444e9e14297da6439dc87f9c65a7# Parent  3b247fa77c6898d200853f52426b3c95505b89cd
merged

diff -r b2073920448f -r 3a7c2c949320 lib/html/isabelle.css
--- a/lib/html/isabelle.css	Sat May 22 16:45:46 2010 -0700
+++ b/lib/html/isabelle.css	Sat May 22 16:46:18 2010 -0700
@@ -1,4 +1,4 @@
-/* css style file for Isabelle XHTML/XML output */
+/* style file for Isabelle XHTML/XML output */
 
 body { background-color: #FFFFFF; }
 
diff -r b2073920448f -r 3a7c2c949320 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat May 22 16:45:46 2010 -0700
+++ b/src/HOL/Library/Multiset.thy	Sat May 22 16:46:18 2010 -0700
@@ -826,7 +826,8 @@
   This lemma shows which properties suffice to show that a function
   @{text "f"} with @{text "f xs = ys"} behaves like sort.
 *}
-lemma properties_for_sort:
+
+lemma (in linorder) properties_for_sort:
   "multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
 proof (induct xs arbitrary: ys)
   case Nil then show ?case by simp
diff -r b2073920448f -r 3a7c2c949320 src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Sat May 22 16:45:46 2010 -0700
+++ b/src/HOL/Library/Quicksort.thy	Sat May 22 16:46:18 2010 -0700
@@ -2,7 +2,7 @@
     Copyright   1994 TU Muenchen
 *)
 
-header{*Quicksort*}
+header {* Quicksort *}
 
 theory Quicksort
 imports Main Multiset
@@ -12,22 +12,27 @@
 begin
 
 fun quicksort :: "'a list \<Rightarrow> 'a list" where
-"quicksort []     = []" |
-"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
+  "quicksort []     = []"
+| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+
+lemma [code]:
+  "quicksort []     = []"
+  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+  by (simp_all add: not_le)
 
 lemma quicksort_permutes [simp]:
   "multiset_of (quicksort xs) = multiset_of xs"
-by (induct xs rule: quicksort.induct) (auto simp: union_ac)
+  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
-by(simp add: set_count_greater_0)
+  by (simp add: set_count_greater_0)
 
-lemma sorted_quicksort: "sorted(quicksort xs)"
-apply (induct xs rule: quicksort.induct)
- apply simp
-apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
-apply (metis leD le_cases le_less_trans)
-done
+lemma sorted_quicksort: "sorted (quicksort xs)"
+  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
+
+theorem quicksort_sort [code_unfold]:
+  "sort = quicksort"
+  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+
 
 end
 
diff -r b2073920448f -r 3a7c2c949320 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Sat May 22 16:45:46 2010 -0700
+++ b/src/HOL/ex/MergeSort.thy	Sat May 22 16:46:18 2010 -0700
@@ -6,7 +6,7 @@
 header{*Merge Sort*}
 
 theory MergeSort
-imports Sorting
+imports Multiset
 begin
 
 context linorder
@@ -19,23 +19,17 @@
 | "merge xs [] = xs"
 | "merge [] ys = ys"
 
-lemma multiset_of_merge[simp]:
-     "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
-apply(induct xs ys rule: merge.induct)
-apply (auto simp: union_ac)
-done
+lemma multiset_of_merge [simp]:
+  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
+  by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
 
-lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
-apply(induct xs ys rule: merge.induct)
-apply auto
-done
+lemma set_merge [simp]:
+  "set (merge xs ys) = set xs \<union> set ys"
+  by (induct xs ys rule: merge.induct) auto
 
-lemma sorted_merge[simp]:
-     "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
-apply(induct xs ys rule: merge.induct)
-apply(simp_all add: ball_Un not_le less_le)
-apply(blast intro: order_trans)
-done
+lemma sorted_merge [simp]:
+  "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
+  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)
 
 fun msort :: "'a list \<Rightarrow> 'a list"
 where
@@ -44,16 +38,19 @@
 | "msort xs = merge (msort (take (size xs div 2) xs))
                     (msort (drop (size xs div 2) xs))"
 
-theorem sorted_msort: "sorted (op \<le>) (msort xs)"
-by (induct xs rule: msort.induct) simp_all
+lemma sorted_msort:
+  "sorted (msort xs)"
+  by (induct xs rule: msort.induct) simp_all
 
-theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
-apply (induct xs rule: msort.induct)
-  apply simp_all
-apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
-done
+lemma multiset_of_msort:
+  "multiset_of (msort xs) = multiset_of xs"
+  by (induct xs rule: msort.induct)
+    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
+
+theorem msort_sort:
+  "sort = msort"
+  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
 
 end
 
-
 end
diff -r b2073920448f -r 3a7c2c949320 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/Concurrent/future.ML	Sat May 22 16:46:18 2010 -0700
@@ -170,12 +170,14 @@
 fun future_job group (e: unit -> 'a) =
   let
     val result = Single_Assignment.var "future" : 'a result;
+    val pos = Position.thread_data ();
     fun job ok =
       let
         val res =
           if ok then
             Exn.capture (fn () =>
-              Multithreading.with_attributes Multithreading.private_interrupts (fn _ => e ())) ()
+              Multithreading.with_attributes Multithreading.private_interrupts
+                (fn _ => Position.setmp_thread_data pos e ())) ()
           else Exn.Exn Exn.Interrupt;
       in assign_result group result res end;
   in (result, job) end;
diff -r b2073920448f -r 3a7c2c949320 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/General/position.ML	Sat May 22 16:46:18 2010 -0700
@@ -173,9 +173,7 @@
 
 fun thread_data () = the_default none (Thread.getLocal tag);
 
-fun setmp_thread_data pos f x =
-  if ! Output.debugging then f x
-  else Library.setmp_thread_data tag (thread_data ()) pos f x;
+fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
 
 end;
 
diff -r b2073920448f -r 3a7c2c949320 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/IsaMakefile	Sat May 22 16:46:18 2010 -0700
@@ -12,8 +12,6 @@
 
 ## global settings
 
-SHELL = /bin/bash
-
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
diff -r b2073920448f -r 3a7c2c949320 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/Isar/calculation.ML	Sat May 22 16:46:18 2010 -0700
@@ -14,7 +14,8 @@
   val sym_del: attribute
   val symmetric: attribute
   val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
-  val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+  val also_cmd: (Facts.ref * Attrib.src list) list option ->
+    bool -> Proof.state -> Proof.state Seq.seq
   val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
   val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.seq
@@ -27,7 +28,7 @@
 
 (** calculation data **)
 
-structure CalculationData = Generic_Data
+structure Data = Generic_Data
 (
   type T = (thm Item_Net.T * thm list) * (thm list * int) option;
   val empty = ((Thm.elim_rules, []), NONE);
@@ -37,7 +38,7 @@
 );
 
 fun print_rules ctxt =
-  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
+  let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
     [Pretty.big_list "transitivity rules:"
         (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
       Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
@@ -48,7 +49,7 @@
 (* access calculation *)
 
 fun get_calculation state =
-  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
+  (case #2 (Data.get (Context.Proof (Proof.context_of state))) of
     NONE => NONE
   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
 
@@ -56,7 +57,7 @@
 
 fun put_calculation calc =
   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
-     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
+     (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
   #> Proof.put_thms false (calculationN, calc);
 
 
@@ -65,22 +66,22 @@
 
 (* add/del rules *)
 
-val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update);
-val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove);
+val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
+val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
 
 val sym_add =
-  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
+  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
   #> Context_Rules.elim_query NONE;
 
 val sym_del =
-  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
+  Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
   #> Context_Rules.rule_del;
 
 
 (* symmetric *)
 
 val symmetric = Thm.rule_attribute (fn x => fn th =>
-  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
+  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
     ([th'], _) => Drule.zero_var_indexes th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
@@ -103,28 +104,31 @@
 
 (** proof commands **)
 
-fun err_if b msg = if b then error msg else ();
-
 fun assert_sane final =
   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
 
-fun maintain_calculation false calc = put_calculation (SOME calc)
-  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
-
-fun print_calculation false _ _ = ()
-  | print_calculation true ctxt calc = Pretty.writeln
-      (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc));
+fun maintain_calculation int final calc state =
+  let
+    val state' = put_calculation (SOME calc) state;
+    val ctxt' = Proof.context_of state';
+    val _ =
+      if int then
+        Pretty.writeln
+          (ProofContext.pretty_fact ctxt'
+            (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
+      else ();
+  in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
 
 
 (* also and finally *)
 
-val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
+val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
 
 fun calculate prep_rules final raw_rules int state =
   let
     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
-    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
+    fun projection ths th = exists (curry eq_prop th) ths;
 
     val opt_rules = Option.map (prep_rules state) raw_rules;
     fun combine ths =
@@ -141,11 +145,12 @@
       (case get_calculation state of
         NONE => (true, Seq.single facts)
       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
+
+    val _ = initial andalso final andalso error "No calculation yet";
+    val _ = initial andalso is_some opt_rules andalso
+      error "Initial calculation -- no rules to be given";
   in
-    err_if (initial andalso final) "No calculation yet";
-    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
-    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
-        state |> maintain_calculation final calc))
+    calculations |> Seq.map (fn calc => maintain_calculation int final calc state)
   end;
 
 val also = calculate (K I) false;
@@ -164,11 +169,8 @@
         NONE => (true, [])
       | SOME thms => (false, thms));
     val calc = thms @ facts;
-  in
-    err_if (initial andalso final) "No calculation yet";
-    print_calculation int (Proof.context_of state) calc;
-    state |> maintain_calculation final calc
-  end;
+    val _ = initial andalso final andalso error "No calculation yet";
+  in maintain_calculation int final calc state end;
 
 val moreover = collect false;
 val ultimately = collect true;
diff -r b2073920448f -r 3a7c2c949320 src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/PIDE/state.scala	Sat May 22 16:46:18 2010 -0700
@@ -74,7 +74,7 @@
   {
     val changed: State =
       message match {
-        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+        case XML.Elem(Markup.STATUS, _, elems) =>
           (this /: elems)((state, elem) =>
             elem match {
               case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
diff -r b2073920448f -r 3a7c2c949320 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/System/isabelle_process.scala	Sat May 22 16:46:18 2010 -0700
@@ -84,7 +84,7 @@
 
   class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
   {
-    def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
+    def message = XML.Elem(Kind.markup(kind), props, body)
 
     override def toString: String =
     {
diff -r b2073920448f -r 3a7c2c949320 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/System/session.scala	Sat May 22 16:46:18 2010 -0700
@@ -104,7 +104,7 @@
 
     def bad_result(result: Isabelle_Process.Result)
     {
-      System.err.println("Ignoring prover result: " + result)
+      System.err.println("Ignoring prover result: " + result.message.toString)
     }
 
     def handle_result(result: Isabelle_Process.Result)
diff -r b2073920448f -r 3a7c2c949320 src/Pure/build-jars
diff -r b2073920448f -r 3a7c2c949320 src/Pure/library.scala
--- a/src/Pure/library.scala	Sat May 22 16:45:46 2010 -0700
+++ b/src/Pure/library.scala	Sat May 22 16:46:18 2010 -0700
@@ -17,6 +17,14 @@
 
 object Library
 {
+  /* partial functions */
+
+  def undefined[A, B] = new PartialFunction[A, B] {
+    def apply(x: A): B = throw new NoSuchElementException("undefined")
+    def isDefinedAt(x: A) = false
+  }
+
+
   /* separate */
 
   def separate[A](s: A, list: List[A]): List[A] =
@@ -94,27 +102,27 @@
 
   /* zoom box */
 
-  def zoom_box(apply_factor: Int => Unit) =
-    new ComboBox(
-      List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) {
-      val Factor = "([0-9]+)%?"r
-      def reset(): Int = { selection.index = 3; 100 }
+  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
+    List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
+  {
+    val Factor = "([0-9]+)%?"r
+    def parse(text: String): Int =
+      text match {
+        case Factor(s) =>
+          val i = Integer.parseInt(s)
+          if (10 <= i && i <= 1000) i else 100
+        case _ => 100
+      }
+    def print(i: Int): String = i.toString + "%"
 
-      reactions += {
-        case SelectionChanged(_) =>
-          val factor =
-            selection.item match {
-              case Factor(s) =>
-                val i = Integer.parseInt(s)
-                if (10 <= i && i <= 1000) i else reset()
-              case _ => reset()
-            }
-          apply_factor(factor)
-        }
-      reset()
-      listenTo(selection)
-      makeEditable()
+    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
+    reactions += {
+      case SelectionChanged(_) => apply_factor(parse(selection.item))
     }
+    listenTo(selection)
+    selection.index = 3
+    prototypeDisplayValue = Some("00000%")
+  }
 
 
   /* timing */
diff -r b2073920448f -r 3a7c2c949320 src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Sat May 22 16:46:18 2010 -0700
@@ -0,0 +1,13 @@
+/* additional style file for Isabelle/jEdit output */
+
+pre.message { margin-top: 0.3ex; background-color: #F0F0F0; }
+
+.writeln { }
+.priority { }
+.tracing { background-color: #EAF8FF; }
+.warning { background-color: #EEE8AA; }
+.error { background-color: #FFC1C1; }
+.debug { background-color: #FFE4E1; }
+
+.hilite { background-color: #FFFACD; }
+
diff -r b2073920448f -r 3a7c2c949320 src/Tools/jEdit/dist-template/modes/isabelle.xml
--- a/src/Tools/jEdit/dist-template/modes/isabelle.xml	Sat May 22 16:45:46 2010 -0700
+++ b/src/Tools/jEdit/dist-template/modes/isabelle.xml	Sat May 22 16:46:18 2010 -0700
@@ -7,10 +7,8 @@
     <PROPERTY NAME="commentStart" VALUE="(*"/>
     <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
-    <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
-    <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
-    <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
-    <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE=")]}" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
diff -r b2073920448f -r 3a7c2c949320 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Sat May 22 16:45:46 2010 -0700
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Sat May 22 16:46:18 2010 -0700
@@ -37,18 +37,17 @@
 }
 
 
-class HTML_Panel(
-  system: Isabelle_System,
-  initial_font_size: Int,
-  handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
+class HTML_Panel(system: Isabelle_System, initial_font_size: Int) extends HtmlPanel
 {
-  // global logging
+  /** Lobo setup **/
+
+  /* global logging */
+
   Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
 
 
-  /* Lobo setup */
+  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
 
-  // pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize
   val screen_resolution =
     if (GraphicsEnvironment.isHeadless()) 72
     else Toolkit.getDefaultToolkit().getScreenResolution()
@@ -57,11 +56,15 @@
   def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
 
 
+  /* contexts and event handling */
+
+  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
+
   private val ucontext = new SimpleUserAgentContext
   private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
   {
     private def handle(event: HTML_Panel.Event): Boolean =
-      if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
+      if (handler.isDefinedAt(event)) { handler(event); true }
       else false
 
     override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
@@ -90,7 +93,9 @@
 <style media="all" type="text/css">
 """ +
   system.try_read("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
-  system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n"
+  system.try_read("$JEDIT_HOME/etc/isabelle-jedit.css") + "\n" +
+  system.try_read("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
+  system.try_read("$ISABELLE_HOME_USER/etc/isabelle-jedit.css") + "\n"
 
   private val template_tail =
 """
@@ -106,26 +111,37 @@
     template_tail
 
 
-  /* physical document */
+  /** main actor **/
+
+  /* internal messages */
+
+  private case class Resize(font_size: Int)
+  private case class Render(body: List[XML.Tree])
+  private case object Refresh
 
-  private class Doc
-  {
-    private var current_font_size: Int = 0
-    private var current_font_metrics: FontMetrics = null
-    private var current_body: List[XML.Tree] = Nil
-    private var current_DOM: org.w3c.dom.Document = null
+  private val main_actor = actor {
+
+    /* internal state */
+
+    var current_font_metrics: FontMetrics = null
+    var current_font_size: Int = 0
+    var current_margin: Int = 0
+    var current_body: List[XML.Tree] = Nil
 
     def resize(font_size: Int)
     {
-      if (font_size != current_font_size || current_font_metrics == null) {
+      val (font_metrics, margin) =
         Swing_Thread.now {
-          current_font_size = font_size
-          current_font_metrics =
-            getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
+          val metrics = getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
+          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
         }
-        current_DOM =
-          builder.parse(
-            new InputSourceImpl(new StringReader(template(font_size)), "http://localhost"))
+      if (current_font_metrics == null ||
+          current_font_size != font_size ||
+          current_margin != margin)
+      {
+        current_font_metrics = font_metrics
+        current_font_size = font_size
+        current_margin = margin
         refresh()
       }
     }
@@ -135,43 +151,36 @@
     def render(body: List[XML.Tree])
     {
       current_body = body
-      val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
       val html_body =
         current_body.flatMap(div =>
-          Pretty.formatted(List(div), margin,
-              Pretty.font_metric(current_font_metrics))
-            .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
+          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
+            .map(t => XML.Elem(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE)), HTML.spans(t))))
+      val doc =
+        builder.parse(
+          new InputSourceImpl(new StringReader(template(current_font_size)), "http://localhost"))
+      doc.removeChild(doc.getLastChild())
+      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
+      Swing_Thread.later { setDocument(doc, rcontext) }
+    }
 
-      val node = XML.document_node(current_DOM, XML.elem(HTML.BODY, html_body))
-      Swing_Thread.now {
-        current_DOM.removeChild(current_DOM.getLastChild())
-        current_DOM.appendChild(node)
-        setDocument(current_DOM, rcontext)
-      }
-    }
+
+    /* main loop */
 
     resize(initial_font_size)
-  }
 
-
-  /* main actor and method wrappers */
-
-  private case class Resize(font_size: Int)
-  private case class Render(body: List[XML.Tree])
-  private case object Refresh
-
-  private val main_actor = actor {
-    var doc = new Doc
     loop {
       react {
-        case Resize(font_size) => doc.resize(font_size)
-        case Refresh => doc.refresh()
-        case Render(body) => doc.render(body)
+        case Resize(font_size) => resize(font_size)
+        case Refresh => refresh()
+        case Render(body) => render(body)
         case bad => System.err.println("main_actor: ignoring bad message " + bad)
       }
     }
   }
 
+
+  /* external methods */
+
   def resize(font_size: Int) { main_actor ! Resize(font_size) }
   def refresh() { main_actor ! Refresh }
   def render(body: List[XML.Tree]) { main_actor ! Render(body) }
diff -r b2073920448f -r 3a7c2c949320 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat May 22 16:45:46 2010 -0700
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat May 22 16:46:18 2010 -0700
@@ -28,15 +28,49 @@
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  val controls = new FlowPanel(FlowPanel.Alignment.Right)()
-  add(controls.peer, BorderLayout.NORTH)
-
-  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
+  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()))
   add(html_panel, BorderLayout.CENTER)
 
 
   /* controls */
 
+  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+  zoom.tooltip = "Zoom factor for basic font size"
+
+  private val update = new Button("Update") {
+    reactions += { case ButtonClicked(_) => handle_update() }
+  }
+  update.tooltip =
+    "<html>Update display according to the<br>state of command at caret position</html>"
+
+  private val tracing = new CheckBox("Tracing") {
+    reactions += { case ButtonClicked(_) => handle_update() }
+  }
+  tracing.tooltip =
+    "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
+
+  private val debug = new CheckBox("Debug") {
+    reactions += { case ButtonClicked(_) => handle_update() }
+  }
+  debug.tooltip =
+    "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
+
+  private val follow = new CheckBox("Follow")
+  follow.selected = true
+  follow.tooltip =
+    "<html>Indicate automatic update following<br>caret movement or state changes</html>"
+
+  private def filtered_results(document: Document, cmd: Command): List[XML.Tree] =
+  {
+    val show_tracing = tracing.selected
+    val show_debug = debug.selected
+    document.current_state(cmd).results filter {
+      case XML.Elem(Markup.TRACING, _, _) => show_tracing
+      case XML.Elem(Markup.DEBUG, _, _) => show_debug
+      case _ => true
+    }
+  }
+
   private case class Render(body: List[XML.Tree])
 
   private def handle_update()
@@ -47,7 +81,7 @@
           val document = model.recent_document
           document.command_at(view.getTextArea.getCaretPosition) match {
             case Some((cmd, _)) =>
-              output_actor ! Render(document.current_state(cmd).results)
+              output_actor ! Render(filtered_results(document, cmd))
             case None =>
           }
         case None =>
@@ -62,15 +96,6 @@
       html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
     }
 
-  private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
-
-  private val update = new Button("Update") {
-    reactions += { case ButtonClicked(_) => handle_update() }
-  }
-
-  private val follow = new CheckBox("Follow")
-  follow.selected = true
-
 
   /* actor wiring */
 
@@ -85,7 +110,8 @@
             if (follow.selected) Document_Model(view.getBuffer) else None
           } match {
             case None =>
-            case Some(model) => html_panel.render(model.recent_document.current_state(cmd).results)
+            case Some(model) =>
+              html_panel.render(filtered_results(model.recent_document, cmd))
           }
 
         case bad => System.err.println("output_actor: ignoring bad message " + bad)
@@ -111,13 +137,15 @@
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(500) { html_panel.refresh() }
+    val delay = Swing_Thread.delay_last(500) { handle_resize() }
     override def componentResized(e: ComponentEvent) { delay() }
   })
 
 
   /* init controls */
 
-  controls.contents ++= List(zoom, update, follow)
+  val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, update, debug, tracing, follow)
+  add(controls.peer, BorderLayout.NORTH)
+
   handle_update()
 }