# HG changeset patch # User wenzelm # Date 1285775960 -7200 # Node ID b1640def6d4450957b49146acd48eb53a108c957 # Parent 533dd8cda12c18548d9580e463bfeef5ef027c12# Parent b59e064e32c3013b31457e8919a00c6f3b428f8c merged diff -r 533dd8cda12c -r b1640def6d44 src/HOLCF/IOA/ABP/Check.ML --- 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 "}"); diff -r 533dd8cda12c -r b1640def6d44 src/Pure/General/output.ML --- 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 => ()); diff -r 533dd8cda12c -r b1640def6d44 src/Pure/ProofGeneral/proof_general_emacs.ML --- 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); diff -r 533dd8cda12c -r b1640def6d44 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 *) diff -r 533dd8cda12c -r b1640def6d44 src/Pure/System/download.scala --- 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) diff -r 533dd8cda12c -r b1640def6d44 src/Pure/System/isabelle_process.ML --- 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; diff -r 533dd8cda12c -r b1640def6d44 src/Pure/System/isabelle_process.scala --- 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") diff -r 533dd8cda12c -r b1640def6d44 src/Pure/System/session.ML --- 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 diff -r 533dd8cda12c -r b1640def6d44 src/Pure/System/standard_system.scala --- 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 = diff -r 533dd8cda12c -r b1640def6d44 src/Pure/Thy/present.ML --- 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; diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/dist-template/README.html --- 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 @@ -Notes on Isabelle/Isar Prover IDE +Notes on the Isabelle/jEdit Prover IDE -

Notes on Isabelle/Isar Prover IDE

+

Notes on the Isabelle/jEdit Prover IDE

diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/dist-template/lib/Tools/jedit --- 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 cat > "$JEDIT_SETTINGS/perspective.xml" < diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/plugin/Isabelle.props --- 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 diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/src/jedit/document_view.scala --- 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 diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/src/jedit/html_panel.scala --- 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) } } diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- 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 diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/src/jedit/isabelle_options.scala --- 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] diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/src/jedit/plugin.scala --- 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 => diff -r 533dd8cda12c -r b1640def6d44 src/Tools/jEdit/src/jedit/session_dockable.scala --- 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)