--- a/src/HOLCF/IOA/ABP/Check.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/HOLCF/IOA/ABP/Check.ML Wed Sep 29 17:59:20 2010 +0200
@@ -112,21 +112,21 @@
------------------------------------*)
fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
- let fun prec x = (Output.std_output ","; pre x)
+ let fun prec x = (Output.raw_stdout ","; pre x)
in
(case lll of
- [] => (Output.std_output lpar; Output.std_output rpar)
- | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
+ [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
+ | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
end;
-fun pr_bool true = Output.std_output "true"
-| pr_bool false = Output.std_output "false";
+fun pr_bool true = Output.raw_stdout "true"
+| pr_bool false = Output.raw_stdout "false";
-fun pr_msg m = Output.std_output "m"
-| pr_msg n = Output.std_output "n"
-| pr_msg l = Output.std_output "l";
+fun pr_msg m = Output.raw_stdout "m"
+| pr_msg n = Output.raw_stdout "n"
+| pr_msg l = Output.raw_stdout "l";
-fun pr_act a = Output.std_output (case a of
+fun pr_act a = Output.raw_stdout (case a of
Next => "Next"|
S_msg(ma) => "S_msg(ma)" |
R_msg(ma) => "R_msg(ma)" |
@@ -135,17 +135,17 @@
S_ack(b) => "S_ack(b)" |
R_ack(b) => "R_ack(b)");
-fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
+fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
val pr_bool_list = print_list("[","]",pr_bool);
val pr_msg_list = print_list("[","]",pr_msg);
val pr_pkt_list = print_list("[","]",pr_pkt);
fun pr_tuple (env,p,a,q,b,ch1,ch2) =
- (Output.std_output "{"; pr_bool env; Output.std_output ", "; pr_msg_list p; Output.std_output ", ";
- pr_bool a; Output.std_output ", "; pr_msg_list q; Output.std_output ", ";
- pr_bool b; Output.std_output ", "; pr_pkt_list ch1; Output.std_output ", ";
- pr_bool_list ch2; Output.std_output "}");
+ (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p; Output.raw_stdout ", ";
+ pr_bool a; Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
+ pr_bool b; Output.raw_stdout ", "; pr_pkt_list ch1; Output.raw_stdout ", ";
+ pr_bool_list ch2; Output.raw_stdout "}");
--- a/src/Pure/General/output.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/General/output.ML Wed Sep 29 17:59:20 2010 +0200
@@ -28,9 +28,9 @@
val output_width: string -> output * int
val output: string -> output
val escape: output -> string
- val std_output: output -> unit
- val std_error: output -> unit
- val writeln_default: output -> unit
+ val raw_stdout: output -> unit
+ val raw_stderr: output -> unit
+ val raw_writeln: output -> unit
val writeln_fn: (output -> unit) Unsynchronized.ref
val priority_fn: (output -> unit) Unsynchronized.ref
val tracing_fn: (output -> unit) Unsynchronized.ref
@@ -77,24 +77,24 @@
(** output channels **)
-(* output primitives -- normally NOT used directly!*)
+(* raw output primitives -- not to be used in user-space *)
-fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
-fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
+fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
+fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
-fun writeln_default "" = ()
- | writeln_default s = std_output (suffix "\n" s);
+fun raw_writeln "" = ()
+ | raw_writeln s = raw_stdout (suffix "\n" s); (*atomic output!*)
(* Isabelle output channels *)
-val writeln_fn = Unsynchronized.ref writeln_default;
+val writeln_fn = Unsynchronized.ref raw_writeln;
val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
-val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
-val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
-val prompt_fn = Unsynchronized.ref std_output;
+val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+val debug_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "::: ");
+val prompt_fn = Unsynchronized.ref raw_stdout;
val status_fn = Unsynchronized.ref (fn _: string => ());
val report_fn = Unsynchronized.ref (fn _: string => ());
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 29 17:59:20 2010 +0200
@@ -71,7 +71,7 @@
fun message bg en prfx text =
(case render text of
"" => ()
- | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
+ | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
fun setup_messages () =
(Output.writeln_fn := message "" "" "";
@@ -81,7 +81,7 @@
Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
Output.warning_fn := message (special "K") (special "L") "### ";
Output.error_fn := message (special "M") (special "N") "*** ";
- Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
+ Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
fun panic s =
(message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 29 17:59:20 2010 +0200
@@ -66,7 +66,7 @@
fun matching_pgip_id id = (id = ! pgip_id)
-val output_xml_fn = Unsynchronized.ref Output.writeln_default
+val output_xml_fn = Unsynchronized.ref Output.raw_writeln
fun output_xml s = ! output_xml_fn (XML.string_of s);
val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
@@ -1032,7 +1032,7 @@
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
local
- val pgip_output_channel = Unsynchronized.ref Output.writeln_default
+ val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
in
(* Set recipient for PGIP results *)
--- a/src/Pure/System/download.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/System/download.scala Wed Sep 29 17:59:20 2010 +0200
@@ -42,7 +42,7 @@
val outstream = new BufferedOutputStream(new FileOutputStream(file))
try {
var c: Int = 0
- while ({ c = read(); c != -1}) outstream.write(c)
+ while ({ c = read(); c != -1 }) outstream.write(c)
}
finally { outstream.close }
if (mod_time > 0) file.setLastModified(mod_time)
--- a/src/Pure/System/isabelle_process.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Sep 29 17:59:20 2010 +0200
@@ -172,7 +172,7 @@
fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
let
val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
- val _ = Output.std_output Symbol.STX;
+ val _ = Output.raw_stdout Symbol.STX;
val _ = quick_and_dirty := true; (* FIXME !? *)
val _ = Context.set_thread_data NONE;
--- a/src/Pure/System/isabelle_process.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Wed Sep 29 17:59:20 2010 +0200
@@ -335,8 +335,8 @@
var m = 0
do {
m = stream.read(buf, i, n - i)
- i += m
- } while (m > 0 && n > i)
+ if (m != -1) i += m
+ } while (m != -1 && n > i)
if (i != n) throw new Protocol_Error("bad message chunk content")
--- a/src/Pure/System/session.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/System/session.ML Wed Sep 29 17:59:20 2010 +0200
@@ -104,7 +104,7 @@
val _ = use root;
val stop = end_timing start;
val _ =
- Output.std_error ("Timing " ^ item ^ " (" ^
+ Output.raw_stderr ("Timing " ^ item ^ " (" ^
string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
#message stop ^ ")\n");
in () end
--- a/src/Pure/System/standard_system.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/System/standard_system.scala Wed Sep 29 17:59:20 2010 +0200
@@ -6,6 +6,7 @@
package isabelle
+import java.util.zip.{ZipEntry, ZipInputStream}
import java.util.regex.Pattern
import java.util.Locale
import java.net.URL
@@ -157,7 +158,37 @@
: (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
- /* unpack tar archive */
+ /* unpack zip archive -- platform file-system */
+
+ def unzip(url: URL, root: File)
+ {
+ import scala.collection.JavaConversions._
+
+ val buffer = new Array[Byte](4096)
+
+ val zip_stream = new ZipInputStream(new BufferedInputStream(url.openStream))
+ var entry: ZipEntry = null
+ try {
+ while ({ entry = zip_stream.getNextEntry; entry != null }) {
+ val file = new File(root, entry.getName.replace('/', File.separatorChar))
+ val dir = file.getParentFile
+ if (dir != null && !dir.isDirectory && !dir.mkdirs)
+ error("Failed to create directory: " + dir)
+
+ var len = 0
+ val out_stream = new BufferedOutputStream(new FileOutputStream(file))
+ try {
+ while ({ len = zip_stream.read(buffer); len != -1 })
+ out_stream.write(buffer, 0, len)
+ }
+ finally { out_stream.close }
+ }
+ }
+ finally { zip_stream.close }
+ }
+
+
+ /* unpack tar archive -- POSIX file-system */
def posix_untar(url: URL, root: File, gunzip: Boolean = false,
tar: String = "tar", gzip: String = "", progress: Int => Unit = _ => ()): String =
--- a/src/Pure/Thy/present.ML Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Pure/Thy/present.ML Wed Sep 29 17:59:20 2010 +0200
@@ -293,7 +293,7 @@
val (doc_prefix1, documents) =
if doc = "" then (NONE, [])
else if not (File.exists document_path) then
- (if verbose then Output.std_error "Warning: missing document directory\n" else ();
+ (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
(NONE, []))
else (SOME (Path.append html_prefix document_path, html_prefix),
read_versions doc_versions);
@@ -409,12 +409,12 @@
File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
List.app finish_html thys;
List.app (uncurry File.write) files;
- if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
+ if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
else ();
(case doc_prefix2 of NONE => () | SOME (cp, path) =>
(prepare_sources cp path;
- if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
+ if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
(case doc_prefix1 of NONE => () | SOME (path, result_path) =>
documents |> List.app (fn (name, tags) =>
@@ -422,7 +422,7 @@
val _ = prepare_sources true path;
val doc_path = isabelle_document true doc_format name tags path result_path;
in
- if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
+ if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
end));
browser_info := empty_browser_info;
--- a/src/Tools/jEdit/dist-template/README.html Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/dist-template/README.html Wed Sep 29 17:59:20 2010 +0200
@@ -4,18 +4,33 @@
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
-<title>Notes on Isabelle/Isar Prover IDE</title>
+<title>Notes on the Isabelle/jEdit Prover IDE</title>
</head>
<body>
-<h1>Notes on Isabelle/Isar Prover IDE</h1>
+<h1>Notes on the Isabelle/jEdit Prover IDE</h1>
<ul>
-<li>FIXME</li>
+<li>The original jEdit look-and-feel is generally preserved, although
+ some default properties have been changed to accommodate Isabelle
+ (e.g. main the text area font).</li>
+
+<li>Formal Isabelle/Isar text is checked asynchronously while editing.
+ The user is in full command of the editor, and the prover refrains
+ from locking portions of the buffer etc.</li>
-<li>FIXME</li>
+<li>Prover feedback works via tooltips, syntax highlighting, colors,
+ boxes etc. based on semantic markup provided by Isabelle in the
+ background.</li>
+
+<li>Using the mouse together with the modifier key <tt>C</tt>
+(<tt>CONTROL</tt> on Linux or Windows,
+ <tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
+
+<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
+ windows by jEdit, which also allows multiple instances.</li>
</ul>
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Sep 29 17:59:20 2010 +0200
@@ -106,7 +106,7 @@
if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
- <DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
+<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
<?xml version="1.0" encoding="UTF-8" ?>
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 29 17:59:20 2010 +0200
@@ -7,12 +7,9 @@
buffer.noTabs=true
buffer.sidekick.keystroke-parse=true
buffer.tabSize=2
-console.dock-position=bottom
console.encoding=UTF-8
console.font=IsabelleText
console.fontsize=14
-console.height=174
-console.width=412
delete-line.shortcut=A+d
delete.shortcut2=C+d
encoding.opt-out.Big5-HKSCS=true
@@ -181,8 +178,9 @@
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
isabelle-output.dock-position=bottom
-isabelle-raw-output.dock-position=bottom
isabelle-session.dock-position=bottom
+isabelle-session.height=174
+isabelle-session.width=412
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
--- a/src/Tools/jEdit/plugin/Isabelle.props Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Wed Sep 29 17:59:20 2010 +0200
@@ -32,6 +32,7 @@
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8000
options.isabelle.startup-timeout=10000
+options.isabelle.auto-start.title=Auto Start
options.isabelle.auto-start=true
#menu actions
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 29 17:59:20 2010 +0200
@@ -12,9 +12,10 @@
import scala.actors.Actor._
-import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
-import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
-import javax.swing.{JPanel, ToolTipManager}
+import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
+import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
+ FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
+import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
import javax.swing.event.{CaretListener, CaretEvent}
import org.gjt.sp.jedit.{jEdit, OperatingSystem}
@@ -30,7 +31,7 @@
private val key = new Object
- def init(model: Document_Model, text_area: TextArea): Document_View =
+ def init(model: Document_Model, text_area: JEditTextArea): Document_View =
{
Swing_Thread.require()
val doc_view = new Document_View(model, text_area)
@@ -39,7 +40,7 @@
doc_view
}
- def apply(text_area: TextArea): Option[Document_View] =
+ def apply(text_area: JEditTextArea): Option[Document_View] =
{
Swing_Thread.require()
text_area.getClientProperty(key) match {
@@ -48,7 +49,7 @@
}
}
- def exit(text_area: TextArea)
+ def exit(text_area: JEditTextArea)
{
Swing_Thread.require()
apply(text_area) match {
@@ -61,7 +62,7 @@
}
-class Document_View(val model: Document_Model, text_area: TextArea)
+class Document_View(val model: Document_Model, text_area: JEditTextArea)
{
private val session = model.session
@@ -109,39 +110,38 @@
}
- /* commands_changed_actor */
+ /* HTML popups */
+
+ private var html_popup: Option[Popup] = None
- private val commands_changed_actor = actor {
- loop {
- react {
- case Session.Commands_Changed(changed) =>
- val buffer = model.buffer
- Isabelle.swing_buffer_lock(buffer) {
- val snapshot = model.snapshot()
+ private def exit_popup() { html_popup.map(_.hide) }
- if (changed.exists(snapshot.node.commands.contains))
- overview.repaint()
+ private val html_panel =
+ new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+ html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
- val visible_range = screen_lines_range()
- val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
- if (visible_cmds.exists(changed)) {
- for {
- line <- 0 until text_area.getVisibleLines
- val start = text_area.getScreenLineStartOffset(line) if start >= 0
- val end = text_area.getScreenLineEndOffset(line) if end >= 0
- val range = proper_line_range(start, end)
- val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
- if line_cmds.exists(changed)
- } text_area.invalidateScreenLineRange(line, line)
+ private def html_panel_resize()
+ {
+ Swing_Thread.now {
+ html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+ }
+ }
- // FIXME danger of deadlock!?
- // FIXME potentially slow!?
- model.buffer.propertiesChanged()
- }
- }
+ private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
+ {
+ exit_popup()
+ val offset = text_area.xyToOffset(x, y)
+ val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
- case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
- }
+ // FIXME snapshot.cumulate
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
+ case Text.Info(_, Some(msg)) #:: _ =>
+ val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
+ html_panel.render_sync(List(msg))
+ Thread.sleep(10) // FIXME !?
+ popup.show
+ html_popup = Some(popup)
+ case _ =>
}
}
@@ -160,19 +160,41 @@
private var highlight_range: Option[(Text.Range, Color)] = None
+
+ /* CONTROL-mouse management */
+
+ private def exit_control()
+ {
+ exit_popup()
+ highlight_range = None
+ }
+
private val focus_listener = new FocusAdapter {
- override def focusLost(e: FocusEvent) { highlight_range = None }
+ override def focusLost(e: FocusEvent) {
+ highlight_range = None // FIXME exit_control !?
+ }
+ }
+
+ private val window_listener = new WindowAdapter {
+ override def windowIconified(e: WindowEvent) { exit_control() }
+ override def windowDeactivated(e: WindowEvent) { exit_control() }
}
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseMoved(e: MouseEvent) {
val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
- if (!model.buffer.isLoaded) highlight_range = None
+ val x = e.getX()
+ val y = e.getY()
+
+ if (!model.buffer.isLoaded) exit_control()
else
Isabelle.swing_buffer_lock(model.buffer) {
+ val snapshot = model.snapshot
+
+ if (control) init_popup(snapshot, x, y)
+
highlight_range map { case (range, _) => invalidate_line_range(range) }
- highlight_range =
- if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
+ highlight_range = if (control) subexp_range(snapshot, x, y) else None
highlight_range map { case (range, _) => invalidate_line_range(range) }
}
}
@@ -296,7 +318,7 @@
// gutter icons
val icons =
- (for (Text.Info(_, Some(icon)) <-
+ (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
yield icon).toList.sortWith(_ >= _)
icons match {
@@ -364,14 +386,24 @@
{
super.paintComponent(gfx)
Swing_Thread.assert()
+
val buffer = model.buffer
Isabelle.buffer_lock(buffer) {
val snapshot = model.snapshot()
+
+ def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
+ {
+ try {
+ val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+ val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+ Some((line1, line2))
+ }
+ catch { case e: ArrayIndexOutOfBoundsException => None }
+ }
for {
(command, start) <- snapshot.node.command_starts
if !command.is_ignored
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+ (line1, line2) <- line_range(command, start)
val y = line_to_y(line1)
val height = HEIGHT * (line2 - line1)
color <- Isabelle_Markup.overview_color(snapshot, command)
@@ -390,6 +422,45 @@
}
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case Session.Commands_Changed(changed) =>
+ val buffer = model.buffer
+ Isabelle.swing_buffer_lock(buffer) {
+ val snapshot = model.snapshot()
+
+ if (changed.exists(snapshot.node.commands.contains))
+ overview.repaint()
+
+ val visible_range = screen_lines_range()
+ val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+ if (visible_cmds.exists(changed)) {
+ for {
+ line <- 0 until text_area.getVisibleLines
+ val start = text_area.getScreenLineStartOffset(line) if start >= 0
+ val end = text_area.getScreenLineEndOffset(line) if end >= 0
+ val range = proper_line_range(start, end)
+ val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+ if line_cmds.exists(changed)
+ } text_area.invalidateScreenLineRange(line, line)
+
+ // FIXME danger of deadlock!?
+ // FIXME potentially slow!?
+ model.buffer.propertiesChanged()
+ }
+ }
+
+ case Session.Global_Settings => html_panel_resize()
+
+ case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+
/* activation */
private def activate()
@@ -398,20 +469,25 @@
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
text_area.getGutter.addExtension(gutter_extension)
text_area.addFocusListener(focus_listener)
+ text_area.getView.addWindowListener(window_listener)
text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
- session.commands_changed += commands_changed_actor
+ session.commands_changed += main_actor
+ session.global_settings += main_actor
}
private def deactivate()
{
- session.commands_changed -= commands_changed_actor
+ session.commands_changed -= main_actor
+ session.global_settings -= main_actor
text_area.removeFocusListener(focus_listener)
+ text_area.getView.removeWindowListener(window_listener)
text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
text_area.removeCaretListener(caret_listener)
text_area.removeLeftOfScrollBar(overview)
text_area.getGutter.removeExtension(gutter_extension)
text_area.getPainter.removeExtension(text_area_extension)
+ exit_popup()
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed Sep 29 17:59:20 2010 +0200
@@ -118,6 +118,7 @@
private case class Resize(font_family: String, font_size: Int)
private case class Render_Document(text: String)
private case class Render(body: XML.Body)
+ private case class Render_Sync(body: XML.Body)
private case object Refresh
private val main_actor = actor {
@@ -188,6 +189,7 @@
case Refresh => refresh()
case Render_Document(text) => render_document(text)
case Render(body) => render(body)
+ case Render_Sync(body) => render(body); reply(())
case bad => System.err.println("main_actor: ignoring bad message " + bad)
}
}
@@ -200,4 +202,5 @@
def refresh() { main_actor ! Refresh }
def render_document(text: String) { main_actor ! Render_Document(text) }
def render(body: XML.Body) { main_actor ! Render(body) }
+ def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
}
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 29 17:59:20 2010 +0200
@@ -84,6 +84,12 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
+ val popup: Markup_Tree.Select[XML.Tree] =
+ {
+ case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
+ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg
+ }
+
val gutter_message: Markup_Tree.Select[Icon] =
{
case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed Sep 29 17:59:20 2010 +0200
@@ -9,12 +9,15 @@
import javax.swing.JSpinner
+import scala.swing.CheckBox
+
import org.gjt.sp.jedit.AbstractOptionPane
class Isabelle_Options extends AbstractOptionPane("isabelle")
{
private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
+ private val auto_start = new CheckBox()
private val relative_font_size = new JSpinner()
private val tooltip_font_size = new JSpinner()
private val tooltip_dismiss_delay = new JSpinner()
@@ -23,26 +26,24 @@
{
addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
- addComponent(Isabelle.Property("relative-font-size.title"), {
- relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
- relative_font_size
- })
+ addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
+ auto_start.selected = Isabelle.Boolean_Property("auto-start")
+
+ relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
+ addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
- addComponent(Isabelle.Property("tooltip-font-size.title"), {
- tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
- tooltip_font_size
- })
+ tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
+ addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
- addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), {
- tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
- tooltip_dismiss_delay
- })
+ tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
+ addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
}
override def _save()
{
- Isabelle.Property("logic") =
- logic_selector.selection.item.name
+ Isabelle.Property("logic") = logic_selector.selection.item.name
+
+ Isabelle.Boolean_Property("auto-start") = auto_start.selected
Isabelle.Int_Property("relative-font-size") =
relative_font_size.getValue().asInstanceOf[Int]
--- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 29 17:59:20 2010 +0200
@@ -223,34 +223,29 @@
{
/* session management */
- private def init_model(buffer: Buffer): Option[Document_Model] =
- {
- Document_Model(buffer) match {
- case Some(model) => model.refresh; Some(model)
- case None =>
- Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
- case Some((_, thy_name)) =>
- Some(Document_Model.init(Isabelle.session, buffer, thy_name))
- case None => None
- }
- }
- }
-
- private def activate_buffer(buffer: Buffer)
+ private def init_model(buffer: Buffer)
{
Isabelle.swing_buffer_lock(buffer) {
- init_model(buffer) match {
- case None =>
- case Some(model) =>
- for (text_area <- Isabelle.jedit_text_areas(buffer)) {
- if (Document_View(text_area).map(_.model) != Some(model))
- Document_View.init(model, text_area)
- }
+ val opt_model =
+ Document_Model(buffer) match {
+ case Some(model) => model.refresh; Some(model)
+ case None =>
+ Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
+ case Some((_, thy_name)) =>
+ Some(Document_Model.init(Isabelle.session, buffer, thy_name))
+ case None => None
+ }
+ }
+ if (opt_model.isDefined) {
+ for (text_area <- Isabelle.jedit_text_areas(buffer)) {
+ if (Document_View(text_area).map(_.model) != opt_model)
+ Document_View.init(opt_model.get, text_area)
+ }
}
}
}
- private def deactivate_buffer(buffer: Buffer)
+ private def exit_model(buffer: Buffer)
{
Isabelle.swing_buffer_lock(buffer) {
Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
@@ -258,17 +253,52 @@
}
}
+ private case class Init_Model(buffer: Buffer)
+ private case class Exit_Model(buffer: Buffer)
+ private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
+ private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
+
private val session_manager = actor {
+ var ready = false
loop {
react {
- case Session.Failed =>
- val text = new scala.swing.TextArea(Isabelle.session.syslog())
- text.editable = false
- Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
+ case phase: Session.Phase =>
+ ready = phase == Session.Ready
+ phase match {
+ case Session.Failed =>
+ Swing_Thread.now {
+ val text = new scala.swing.TextArea(Isabelle.session.syslog())
+ text.editable = false
+ Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
+ }
+
+ case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
+ case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
+ case _ =>
+ }
+
+ case Init_Model(buffer) =>
+ if (ready) init_model(buffer)
- case Session.Ready => Isabelle.jedit_buffers.foreach(activate_buffer)
- case Session.Shutdown => Isabelle.jedit_buffers.foreach(deactivate_buffer)
- case _ =>
+ case Exit_Model(buffer) =>
+ exit_model(buffer)
+
+ case Init_View(buffer, text_area) =>
+ if (ready) {
+ Isabelle.swing_buffer_lock(buffer) {
+ Document_Model(buffer) match {
+ case Some(model) => Document_View.init(model, text_area)
+ case None =>
+ }
+ }
+ }
+
+ case Exit_View(buffer, text_area) =>
+ Isabelle.swing_buffer_lock(buffer) {
+ Document_View.exit(text_area)
+ }
+
+ case bad => System.err.println("session_manager: ignoring bad message " + bad)
}
}
}
@@ -283,15 +313,13 @@
if Isabelle.Boolean_Property("auto-start") => Isabelle.start_session()
case msg: BufferUpdate
- if Isabelle.session.phase == Session.Ready && // FIXME race!?
- msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+ if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
val buffer = msg.getBuffer
- if (buffer != null) activate_buffer(buffer)
+ if (buffer != null) session_manager ! Init_Model(buffer)
case msg: EditPaneUpdate
- if Isabelle.session.phase == Session.Ready && // FIXME race!?
- (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
+ if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED ||
msg.getWhat == EditPaneUpdate.DESTROYED) =>
@@ -301,18 +329,11 @@
val text_area = edit_pane.getTextArea
if (buffer != null && text_area != null) {
- Isabelle.swing_buffer_lock(buffer) {
- msg.getWhat match {
- case EditPaneUpdate.BUFFER_CHANGING | EditPaneUpdate.DESTROYED =>
- Document_View.exit(text_area)
- case EditPaneUpdate.BUFFER_CHANGED | EditPaneUpdate.CREATED =>
- Document_Model(buffer) match {
- case Some(model) => Document_View.init(model, text_area)
- case None =>
- }
- case _ =>
- }
- }
+ if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
+ msg.getWhat == EditPaneUpdate.CREATED)
+ session_manager ! Init_View(buffer, text_area)
+ else
+ session_manager ! Exit_View(buffer, text_area)
}
case msg: PropertiesChanged =>
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 29 11:55:08 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 29 17:59:20 2010 +0200
@@ -10,8 +10,7 @@
import isabelle._
import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
- Component, Swing, CheckBox}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
import scala.swing.event.{ButtonClicked, SelectionChanged}
import java.awt.BorderLayout
@@ -24,7 +23,7 @@
{
/* main tabs */
- private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
+ private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
private val syslog = new TextArea(Isabelle.session.syslog())
@@ -55,14 +54,10 @@
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"
- private val auto_start = new CheckBox("Auto start") {
- selected = Isabelle.Boolean_Property("auto-start")
- reactions += {
- case ButtonClicked(_) =>
- Isabelle.Boolean_Property("auto-start") = selected
- if (selected) Isabelle.start_session()
- }
+ private val interrupt = new Button("Interrupt") {
+ reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
}
+ interrupt.tooltip = "Broadcast interrupt to all prover tasks"
private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
logic.listenTo(logic.selection)
@@ -70,13 +65,8 @@
case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
}
- private val interrupt = new Button("Interrupt") {
- reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
- }
- interrupt.tooltip = "Broadcast interrupt to all prover tasks"
-
private val controls =
- new FlowPanel(FlowPanel.Alignment.Right)(session_phase, auto_start, logic, interrupt)
+ new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
add(controls.peer, BorderLayout.NORTH)