--- 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; }
--- 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
--- 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
--- 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
--- 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;
--- 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;
--- 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
--- 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;
--- 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)
--- 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 =
{
--- 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)
--- 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 */
--- /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; }
+
--- 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>
--- 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) }
--- 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()
}