--- a/lib/html/isabelle.css Fri May 21 17:16:16 2010 +0200
+++ b/lib/html/isabelle.css Fri May 21 23:21:40 2010 +0200
@@ -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/Pure/Concurrent/future.ML Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/Concurrent/future.ML Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/General/position.ML Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/IsaMakefile Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/Isar/calculation.ML Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/PIDE/state.scala Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/System/session.scala Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Pure/library.scala Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 23:21:40 2010 +0200
@@ -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/src/jedit/html_panel.scala Fri May 21 17:16:16 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Fri May 21 23:21:40 2010 +0200
@@ -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 Fri May 21 17:16:16 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 23:21:40 2010 +0200
@@ -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()
}