1.1 --- a/src/HOLCF/IOA/ABP/Check.ML Wed Sep 29 11:55:08 2010 +0200
1.2 +++ b/src/HOLCF/IOA/ABP/Check.ML Wed Sep 29 17:59:20 2010 +0200
1.3 @@ -112,21 +112,21 @@
1.4 ------------------------------------*)
1.5
1.6 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
1.7 - let fun prec x = (Output.std_output ","; pre x)
1.8 + let fun prec x = (Output.raw_stdout ","; pre x)
1.9 in
1.10 (case lll of
1.11 - [] => (Output.std_output lpar; Output.std_output rpar)
1.12 - | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
1.13 + [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
1.14 + | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
1.15 end;
1.16
1.17 -fun pr_bool true = Output.std_output "true"
1.18 -| pr_bool false = Output.std_output "false";
1.19 +fun pr_bool true = Output.raw_stdout "true"
1.20 +| pr_bool false = Output.raw_stdout "false";
1.21
1.22 -fun pr_msg m = Output.std_output "m"
1.23 -| pr_msg n = Output.std_output "n"
1.24 -| pr_msg l = Output.std_output "l";
1.25 +fun pr_msg m = Output.raw_stdout "m"
1.26 +| pr_msg n = Output.raw_stdout "n"
1.27 +| pr_msg l = Output.raw_stdout "l";
1.28
1.29 -fun pr_act a = Output.std_output (case a of
1.30 +fun pr_act a = Output.raw_stdout (case a of
1.31 Next => "Next"|
1.32 S_msg(ma) => "S_msg(ma)" |
1.33 R_msg(ma) => "R_msg(ma)" |
1.34 @@ -135,17 +135,17 @@
1.35 S_ack(b) => "S_ack(b)" |
1.36 R_ack(b) => "R_ack(b)");
1.37
1.38 -fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
1.39 +fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
1.40
1.41 val pr_bool_list = print_list("[","]",pr_bool);
1.42 val pr_msg_list = print_list("[","]",pr_msg);
1.43 val pr_pkt_list = print_list("[","]",pr_pkt);
1.44
1.45 fun pr_tuple (env,p,a,q,b,ch1,ch2) =
1.46 - (Output.std_output "{"; pr_bool env; Output.std_output ", "; pr_msg_list p; Output.std_output ", ";
1.47 - pr_bool a; Output.std_output ", "; pr_msg_list q; Output.std_output ", ";
1.48 - pr_bool b; Output.std_output ", "; pr_pkt_list ch1; Output.std_output ", ";
1.49 - pr_bool_list ch2; Output.std_output "}");
1.50 + (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p; Output.raw_stdout ", ";
1.51 + pr_bool a; Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
1.52 + pr_bool b; Output.raw_stdout ", "; pr_pkt_list ch1; Output.raw_stdout ", ";
1.53 + pr_bool_list ch2; Output.raw_stdout "}");
1.54
1.55
1.56
2.1 --- a/src/Pure/General/output.ML Wed Sep 29 11:55:08 2010 +0200
2.2 +++ b/src/Pure/General/output.ML Wed Sep 29 17:59:20 2010 +0200
2.3 @@ -28,9 +28,9 @@
2.4 val output_width: string -> output * int
2.5 val output: string -> output
2.6 val escape: output -> string
2.7 - val std_output: output -> unit
2.8 - val std_error: output -> unit
2.9 - val writeln_default: output -> unit
2.10 + val raw_stdout: output -> unit
2.11 + val raw_stderr: output -> unit
2.12 + val raw_writeln: output -> unit
2.13 val writeln_fn: (output -> unit) Unsynchronized.ref
2.14 val priority_fn: (output -> unit) Unsynchronized.ref
2.15 val tracing_fn: (output -> unit) Unsynchronized.ref
2.16 @@ -77,24 +77,24 @@
2.17
2.18 (** output channels **)
2.19
2.20 -(* output primitives -- normally NOT used directly!*)
2.21 +(* raw output primitives -- not to be used in user-space *)
2.22
2.23 -fun std_output s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
2.24 -fun std_error s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
2.25 +fun raw_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
2.26 +fun raw_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
2.27
2.28 -fun writeln_default "" = ()
2.29 - | writeln_default s = std_output (suffix "\n" s);
2.30 +fun raw_writeln "" = ()
2.31 + | raw_writeln s = raw_stdout (suffix "\n" s); (*atomic output!*)
2.32
2.33
2.34 (* Isabelle output channels *)
2.35
2.36 -val writeln_fn = Unsynchronized.ref writeln_default;
2.37 +val writeln_fn = Unsynchronized.ref raw_writeln;
2.38 val priority_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
2.39 val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
2.40 -val warning_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "### ");
2.41 -val error_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "*** ");
2.42 -val debug_fn = Unsynchronized.ref (std_output o suffix "\n" o prefix_lines "::: ");
2.43 -val prompt_fn = Unsynchronized.ref std_output;
2.44 +val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
2.45 +val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
2.46 +val debug_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "::: ");
2.47 +val prompt_fn = Unsynchronized.ref raw_stdout;
2.48 val status_fn = Unsynchronized.ref (fn _: string => ());
2.49 val report_fn = Unsynchronized.ref (fn _: string => ());
2.50
3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 29 11:55:08 2010 +0200
3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 29 17:59:20 2010 +0200
3.3 @@ -71,7 +71,7 @@
3.4 fun message bg en prfx text =
3.5 (case render text of
3.6 "" => ()
3.7 - | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
3.8 + | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
3.9
3.10 fun setup_messages () =
3.11 (Output.writeln_fn := message "" "" "";
3.12 @@ -81,7 +81,7 @@
3.13 Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
3.14 Output.warning_fn := message (special "K") (special "L") "### ";
3.15 Output.error_fn := message (special "M") (special "N") "*** ";
3.16 - Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
3.17 + Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
3.18
3.19 fun panic s =
3.20 (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 29 11:55:08 2010 +0200
4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Sep 29 17:59:20 2010 +0200
4.3 @@ -66,7 +66,7 @@
4.4
4.5 fun matching_pgip_id id = (id = ! pgip_id)
4.6
4.7 -val output_xml_fn = Unsynchronized.ref Output.writeln_default
4.8 +val output_xml_fn = Unsynchronized.ref Output.raw_writeln
4.9 fun output_xml s = ! output_xml_fn (XML.string_of s);
4.10
4.11 val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
4.12 @@ -1032,7 +1032,7 @@
4.13 (** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
4.14
4.15 local
4.16 - val pgip_output_channel = Unsynchronized.ref Output.writeln_default
4.17 + val pgip_output_channel = Unsynchronized.ref Output.raw_writeln
4.18 in
4.19
4.20 (* Set recipient for PGIP results *)
5.1 --- a/src/Pure/System/download.scala Wed Sep 29 11:55:08 2010 +0200
5.2 +++ b/src/Pure/System/download.scala Wed Sep 29 17:59:20 2010 +0200
5.3 @@ -42,7 +42,7 @@
5.4 val outstream = new BufferedOutputStream(new FileOutputStream(file))
5.5 try {
5.6 var c: Int = 0
5.7 - while ({ c = read(); c != -1}) outstream.write(c)
5.8 + while ({ c = read(); c != -1 }) outstream.write(c)
5.9 }
5.10 finally { outstream.close }
5.11 if (mod_time > 0) file.setLastModified(mod_time)
6.1 --- a/src/Pure/System/isabelle_process.ML Wed Sep 29 11:55:08 2010 +0200
6.2 +++ b/src/Pure/System/isabelle_process.ML Wed Sep 29 17:59:20 2010 +0200
6.3 @@ -172,7 +172,7 @@
6.4 fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
6.5 let
6.6 val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
6.7 - val _ = Output.std_output Symbol.STX;
6.8 + val _ = Output.raw_stdout Symbol.STX;
6.9
6.10 val _ = quick_and_dirty := true; (* FIXME !? *)
6.11 val _ = Context.set_thread_data NONE;
7.1 --- a/src/Pure/System/isabelle_process.scala Wed Sep 29 11:55:08 2010 +0200
7.2 +++ b/src/Pure/System/isabelle_process.scala Wed Sep 29 17:59:20 2010 +0200
7.3 @@ -335,8 +335,8 @@
7.4 var m = 0
7.5 do {
7.6 m = stream.read(buf, i, n - i)
7.7 - i += m
7.8 - } while (m > 0 && n > i)
7.9 + if (m != -1) i += m
7.10 + } while (m != -1 && n > i)
7.11
7.12 if (i != n) throw new Protocol_Error("bad message chunk content")
7.13
8.1 --- a/src/Pure/System/session.ML Wed Sep 29 11:55:08 2010 +0200
8.2 +++ b/src/Pure/System/session.ML Wed Sep 29 17:59:20 2010 +0200
8.3 @@ -104,7 +104,7 @@
8.4 val _ = use root;
8.5 val stop = end_timing start;
8.6 val _ =
8.7 - Output.std_error ("Timing " ^ item ^ " (" ^
8.8 + Output.raw_stderr ("Timing " ^ item ^ " (" ^
8.9 string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
8.10 #message stop ^ ")\n");
8.11 in () end
9.1 --- a/src/Pure/System/standard_system.scala Wed Sep 29 11:55:08 2010 +0200
9.2 +++ b/src/Pure/System/standard_system.scala Wed Sep 29 17:59:20 2010 +0200
9.3 @@ -6,6 +6,7 @@
9.4
9.5 package isabelle
9.6
9.7 +import java.util.zip.{ZipEntry, ZipInputStream}
9.8 import java.util.regex.Pattern
9.9 import java.util.Locale
9.10 import java.net.URL
9.11 @@ -157,7 +158,37 @@
9.12 : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
9.13
9.14
9.15 - /* unpack tar archive */
9.16 + /* unpack zip archive -- platform file-system */
9.17 +
9.18 + def unzip(url: URL, root: File)
9.19 + {
9.20 + import scala.collection.JavaConversions._
9.21 +
9.22 + val buffer = new Array[Byte](4096)
9.23 +
9.24 + val zip_stream = new ZipInputStream(new BufferedInputStream(url.openStream))
9.25 + var entry: ZipEntry = null
9.26 + try {
9.27 + while ({ entry = zip_stream.getNextEntry; entry != null }) {
9.28 + val file = new File(root, entry.getName.replace('/', File.separatorChar))
9.29 + val dir = file.getParentFile
9.30 + if (dir != null && !dir.isDirectory && !dir.mkdirs)
9.31 + error("Failed to create directory: " + dir)
9.32 +
9.33 + var len = 0
9.34 + val out_stream = new BufferedOutputStream(new FileOutputStream(file))
9.35 + try {
9.36 + while ({ len = zip_stream.read(buffer); len != -1 })
9.37 + out_stream.write(buffer, 0, len)
9.38 + }
9.39 + finally { out_stream.close }
9.40 + }
9.41 + }
9.42 + finally { zip_stream.close }
9.43 + }
9.44 +
9.45 +
9.46 + /* unpack tar archive -- POSIX file-system */
9.47
9.48 def posix_untar(url: URL, root: File, gunzip: Boolean = false,
9.49 tar: String = "tar", gzip: String = "", progress: Int => Unit = _ => ()): String =
10.1 --- a/src/Pure/Thy/present.ML Wed Sep 29 11:55:08 2010 +0200
10.2 +++ b/src/Pure/Thy/present.ML Wed Sep 29 17:59:20 2010 +0200
10.3 @@ -293,7 +293,7 @@
10.4 val (doc_prefix1, documents) =
10.5 if doc = "" then (NONE, [])
10.6 else if not (File.exists document_path) then
10.7 - (if verbose then Output.std_error "Warning: missing document directory\n" else ();
10.8 + (if verbose then Output.raw_stderr "Warning: missing document directory\n" else ();
10.9 (NONE, []))
10.10 else (SOME (Path.append html_prefix document_path, html_prefix),
10.11 read_versions doc_versions);
10.12 @@ -409,12 +409,12 @@
10.13 File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
10.14 List.app finish_html thys;
10.15 List.app (uncurry File.write) files;
10.16 - if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
10.17 + if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
10.18 else ();
10.19
10.20 (case doc_prefix2 of NONE => () | SOME (cp, path) =>
10.21 (prepare_sources cp path;
10.22 - if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
10.23 + if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
10.24
10.25 (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
10.26 documents |> List.app (fn (name, tags) =>
10.27 @@ -422,7 +422,7 @@
10.28 val _ = prepare_sources true path;
10.29 val doc_path = isabelle_document true doc_format name tags path result_path;
10.30 in
10.31 - if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
10.32 + if verbose then Output.raw_stderr ("Document at " ^ show_path doc_path ^ "\n") else ()
10.33 end));
10.34
10.35 browser_info := empty_browser_info;
11.1 --- a/src/Tools/jEdit/dist-template/README.html Wed Sep 29 11:55:08 2010 +0200
11.2 +++ b/src/Tools/jEdit/dist-template/README.html Wed Sep 29 17:59:20 2010 +0200
11.3 @@ -4,18 +4,33 @@
11.4
11.5 <head>
11.6 <meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
11.7 -<title>Notes on Isabelle/Isar Prover IDE</title>
11.8 +<title>Notes on the Isabelle/jEdit Prover IDE</title>
11.9 </head>
11.10
11.11 <body>
11.12
11.13 -<h1>Notes on Isabelle/Isar Prover IDE</h1>
11.14 +<h1>Notes on the Isabelle/jEdit Prover IDE</h1>
11.15
11.16 <ul>
11.17
11.18 -<li>FIXME</li>
11.19 +<li>The original jEdit look-and-feel is generally preserved, although
11.20 + some default properties have been changed to accommodate Isabelle
11.21 + (e.g. main the text area font).</li>
11.22
11.23 -<li>FIXME</li>
11.24 +<li>Formal Isabelle/Isar text is checked asynchronously while editing.
11.25 + The user is in full command of the editor, and the prover refrains
11.26 + from locking portions of the buffer etc.</li>
11.27 +
11.28 +<li>Prover feedback works via tooltips, syntax highlighting, colors,
11.29 + boxes etc. based on semantic markup provided by Isabelle in the
11.30 + background.</li>
11.31 +
11.32 +<li>Using the mouse together with the modifier key <tt>C</tt>
11.33 +(<tt>CONTROL</tt> on Linux or Windows,
11.34 + <tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
11.35 +
11.36 +<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
11.37 + windows by jEdit, which also allows multiple instances.</li>
11.38
11.39 </ul>
11.40
12.1 --- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Sep 29 11:55:08 2010 +0200
12.2 +++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Sep 29 17:59:20 2010 +0200
12.3 @@ -106,7 +106,7 @@
12.4
12.5 if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
12.6 cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
12.7 - <DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
12.8 +<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
12.9 EOF
12.10 cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
12.11 <?xml version="1.0" encoding="UTF-8" ?>
13.1 --- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 29 11:55:08 2010 +0200
13.2 +++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 29 17:59:20 2010 +0200
13.3 @@ -7,12 +7,9 @@
13.4 buffer.noTabs=true
13.5 buffer.sidekick.keystroke-parse=true
13.6 buffer.tabSize=2
13.7 -console.dock-position=bottom
13.8 console.encoding=UTF-8
13.9 console.font=IsabelleText
13.10 console.fontsize=14
13.11 -console.height=174
13.12 -console.width=412
13.13 delete-line.shortcut=A+d
13.14 delete.shortcut2=C+d
13.15 encoding.opt-out.Big5-HKSCS=true
13.16 @@ -181,8 +178,9 @@
13.17 insert-newline-indent.shortcut=
13.18 insert-newline.shortcut=ENTER
13.19 isabelle-output.dock-position=bottom
13.20 -isabelle-raw-output.dock-position=bottom
13.21 isabelle-session.dock-position=bottom
13.22 +isabelle-session.height=174
13.23 +isabelle-session.width=412
13.24 line-end.shortcut=END
13.25 line-home.shortcut=HOME
13.26 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
14.1 --- a/src/Tools/jEdit/plugin/Isabelle.props Wed Sep 29 11:55:08 2010 +0200
14.2 +++ b/src/Tools/jEdit/plugin/Isabelle.props Wed Sep 29 17:59:20 2010 +0200
14.3 @@ -32,6 +32,7 @@
14.4 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
14.5 options.isabelle.tooltip-dismiss-delay=8000
14.6 options.isabelle.startup-timeout=10000
14.7 +options.isabelle.auto-start.title=Auto Start
14.8 options.isabelle.auto-start=true
14.9
14.10 #menu actions
15.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 29 11:55:08 2010 +0200
15.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 29 17:59:20 2010 +0200
15.3 @@ -12,9 +12,10 @@
15.4
15.5 import scala.actors.Actor._
15.6
15.7 -import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
15.8 -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
15.9 -import javax.swing.{JPanel, ToolTipManager}
15.10 +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
15.11 +import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
15.12 + FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
15.13 +import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
15.14 import javax.swing.event.{CaretListener, CaretEvent}
15.15
15.16 import org.gjt.sp.jedit.{jEdit, OperatingSystem}
15.17 @@ -30,7 +31,7 @@
15.18
15.19 private val key = new Object
15.20
15.21 - def init(model: Document_Model, text_area: TextArea): Document_View =
15.22 + def init(model: Document_Model, text_area: JEditTextArea): Document_View =
15.23 {
15.24 Swing_Thread.require()
15.25 val doc_view = new Document_View(model, text_area)
15.26 @@ -39,7 +40,7 @@
15.27 doc_view
15.28 }
15.29
15.30 - def apply(text_area: TextArea): Option[Document_View] =
15.31 + def apply(text_area: JEditTextArea): Option[Document_View] =
15.32 {
15.33 Swing_Thread.require()
15.34 text_area.getClientProperty(key) match {
15.35 @@ -48,7 +49,7 @@
15.36 }
15.37 }
15.38
15.39 - def exit(text_area: TextArea)
15.40 + def exit(text_area: JEditTextArea)
15.41 {
15.42 Swing_Thread.require()
15.43 apply(text_area) match {
15.44 @@ -61,7 +62,7 @@
15.45 }
15.46
15.47
15.48 -class Document_View(val model: Document_Model, text_area: TextArea)
15.49 +class Document_View(val model: Document_Model, text_area: JEditTextArea)
15.50 {
15.51 private val session = model.session
15.52
15.53 @@ -109,39 +110,38 @@
15.54 }
15.55
15.56
15.57 - /* commands_changed_actor */
15.58 + /* HTML popups */
15.59
15.60 - private val commands_changed_actor = actor {
15.61 - loop {
15.62 - react {
15.63 - case Session.Commands_Changed(changed) =>
15.64 - val buffer = model.buffer
15.65 - Isabelle.swing_buffer_lock(buffer) {
15.66 - val snapshot = model.snapshot()
15.67 + private var html_popup: Option[Popup] = None
15.68
15.69 - if (changed.exists(snapshot.node.commands.contains))
15.70 - overview.repaint()
15.71 + private def exit_popup() { html_popup.map(_.hide) }
15.72
15.73 - val visible_range = screen_lines_range()
15.74 - val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
15.75 - if (visible_cmds.exists(changed)) {
15.76 - for {
15.77 - line <- 0 until text_area.getVisibleLines
15.78 - val start = text_area.getScreenLineStartOffset(line) if start >= 0
15.79 - val end = text_area.getScreenLineEndOffset(line) if end >= 0
15.80 - val range = proper_line_range(start, end)
15.81 - val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
15.82 - if line_cmds.exists(changed)
15.83 - } text_area.invalidateScreenLineRange(line, line)
15.84 + private val html_panel =
15.85 + new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
15.86 + html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
15.87
15.88 - // FIXME danger of deadlock!?
15.89 - // FIXME potentially slow!?
15.90 - model.buffer.propertiesChanged()
15.91 - }
15.92 - }
15.93 + private def html_panel_resize()
15.94 + {
15.95 + Swing_Thread.now {
15.96 + html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
15.97 + }
15.98 + }
15.99
15.100 - case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
15.101 - }
15.102 + private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
15.103 + {
15.104 + exit_popup()
15.105 + val offset = text_area.xyToOffset(x, y)
15.106 + val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
15.107 +
15.108 + // FIXME snapshot.cumulate
15.109 + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
15.110 + case Text.Info(_, Some(msg)) #:: _ =>
15.111 + val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
15.112 + html_panel.render_sync(List(msg))
15.113 + Thread.sleep(10) // FIXME !?
15.114 + popup.show
15.115 + html_popup = Some(popup)
15.116 + case _ =>
15.117 }
15.118 }
15.119
15.120 @@ -160,19 +160,41 @@
15.121
15.122 private var highlight_range: Option[(Text.Range, Color)] = None
15.123
15.124 +
15.125 + /* CONTROL-mouse management */
15.126 +
15.127 + private def exit_control()
15.128 + {
15.129 + exit_popup()
15.130 + highlight_range = None
15.131 + }
15.132 +
15.133 private val focus_listener = new FocusAdapter {
15.134 - override def focusLost(e: FocusEvent) { highlight_range = None }
15.135 + override def focusLost(e: FocusEvent) {
15.136 + highlight_range = None // FIXME exit_control !?
15.137 + }
15.138 + }
15.139 +
15.140 + private val window_listener = new WindowAdapter {
15.141 + override def windowIconified(e: WindowEvent) { exit_control() }
15.142 + override def windowDeactivated(e: WindowEvent) { exit_control() }
15.143 }
15.144
15.145 private val mouse_motion_listener = new MouseMotionAdapter {
15.146 override def mouseMoved(e: MouseEvent) {
15.147 val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
15.148 - if (!model.buffer.isLoaded) highlight_range = None
15.149 + val x = e.getX()
15.150 + val y = e.getY()
15.151 +
15.152 + if (!model.buffer.isLoaded) exit_control()
15.153 else
15.154 Isabelle.swing_buffer_lock(model.buffer) {
15.155 + val snapshot = model.snapshot
15.156 +
15.157 + if (control) init_popup(snapshot, x, y)
15.158 +
15.159 highlight_range map { case (range, _) => invalidate_line_range(range) }
15.160 - highlight_range =
15.161 - if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
15.162 + highlight_range = if (control) subexp_range(snapshot, x, y) else None
15.163 highlight_range map { case (range, _) => invalidate_line_range(range) }
15.164 }
15.165 }
15.166 @@ -296,7 +318,7 @@
15.167
15.168 // gutter icons
15.169 val icons =
15.170 - (for (Text.Info(_, Some(icon)) <-
15.171 + (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
15.172 snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
15.173 yield icon).toList.sortWith(_ >= _)
15.174 icons match {
15.175 @@ -364,14 +386,24 @@
15.176 {
15.177 super.paintComponent(gfx)
15.178 Swing_Thread.assert()
15.179 +
15.180 val buffer = model.buffer
15.181 Isabelle.buffer_lock(buffer) {
15.182 val snapshot = model.snapshot()
15.183 +
15.184 + def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
15.185 + {
15.186 + try {
15.187 + val line1 = buffer.getLineOfOffset(snapshot.convert(start))
15.188 + val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
15.189 + Some((line1, line2))
15.190 + }
15.191 + catch { case e: ArrayIndexOutOfBoundsException => None }
15.192 + }
15.193 for {
15.194 (command, start) <- snapshot.node.command_starts
15.195 if !command.is_ignored
15.196 - val line1 = buffer.getLineOfOffset(snapshot.convert(start))
15.197 - val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
15.198 + (line1, line2) <- line_range(command, start)
15.199 val y = line_to_y(line1)
15.200 val height = HEIGHT * (line2 - line1)
15.201 color <- Isabelle_Markup.overview_color(snapshot, command)
15.202 @@ -390,6 +422,45 @@
15.203 }
15.204
15.205
15.206 + /* main actor */
15.207 +
15.208 + private val main_actor = actor {
15.209 + loop {
15.210 + react {
15.211 + case Session.Commands_Changed(changed) =>
15.212 + val buffer = model.buffer
15.213 + Isabelle.swing_buffer_lock(buffer) {
15.214 + val snapshot = model.snapshot()
15.215 +
15.216 + if (changed.exists(snapshot.node.commands.contains))
15.217 + overview.repaint()
15.218 +
15.219 + val visible_range = screen_lines_range()
15.220 + val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
15.221 + if (visible_cmds.exists(changed)) {
15.222 + for {
15.223 + line <- 0 until text_area.getVisibleLines
15.224 + val start = text_area.getScreenLineStartOffset(line) if start >= 0
15.225 + val end = text_area.getScreenLineEndOffset(line) if end >= 0
15.226 + val range = proper_line_range(start, end)
15.227 + val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
15.228 + if line_cmds.exists(changed)
15.229 + } text_area.invalidateScreenLineRange(line, line)
15.230 +
15.231 + // FIXME danger of deadlock!?
15.232 + // FIXME potentially slow!?
15.233 + model.buffer.propertiesChanged()
15.234 + }
15.235 + }
15.236 +
15.237 + case Session.Global_Settings => html_panel_resize()
15.238 +
15.239 + case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
15.240 + }
15.241 + }
15.242 + }
15.243 +
15.244 +
15.245 /* activation */
15.246
15.247 private def activate()
15.248 @@ -398,20 +469,25 @@
15.249 addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
15.250 text_area.getGutter.addExtension(gutter_extension)
15.251 text_area.addFocusListener(focus_listener)
15.252 + text_area.getView.addWindowListener(window_listener)
15.253 text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
15.254 text_area.addCaretListener(caret_listener)
15.255 text_area.addLeftOfScrollBar(overview)
15.256 - session.commands_changed += commands_changed_actor
15.257 + session.commands_changed += main_actor
15.258 + session.global_settings += main_actor
15.259 }
15.260
15.261 private def deactivate()
15.262 {
15.263 - session.commands_changed -= commands_changed_actor
15.264 + session.commands_changed -= main_actor
15.265 + session.global_settings -= main_actor
15.266 text_area.removeFocusListener(focus_listener)
15.267 + text_area.getView.removeWindowListener(window_listener)
15.268 text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
15.269 text_area.removeCaretListener(caret_listener)
15.270 text_area.removeLeftOfScrollBar(overview)
15.271 text_area.getGutter.removeExtension(gutter_extension)
15.272 text_area.getPainter.removeExtension(text_area_extension)
15.273 + exit_popup()
15.274 }
15.275 }
15.276 \ No newline at end of file
16.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed Sep 29 11:55:08 2010 +0200
16.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed Sep 29 17:59:20 2010 +0200
16.3 @@ -118,6 +118,7 @@
16.4 private case class Resize(font_family: String, font_size: Int)
16.5 private case class Render_Document(text: String)
16.6 private case class Render(body: XML.Body)
16.7 + private case class Render_Sync(body: XML.Body)
16.8 private case object Refresh
16.9
16.10 private val main_actor = actor {
16.11 @@ -188,6 +189,7 @@
16.12 case Refresh => refresh()
16.13 case Render_Document(text) => render_document(text)
16.14 case Render(body) => render(body)
16.15 + case Render_Sync(body) => render(body); reply(())
16.16 case bad => System.err.println("main_actor: ignoring bad message " + bad)
16.17 }
16.18 }
16.19 @@ -200,4 +202,5 @@
16.20 def refresh() { main_actor ! Refresh }
16.21 def render_document(text: String) { main_actor ! Render_Document(text) }
16.22 def render(body: XML.Body) { main_actor ! Render(body) }
16.23 + def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
16.24 }
17.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 29 11:55:08 2010 +0200
17.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 29 17:59:20 2010 +0200
17.3 @@ -84,6 +84,12 @@
17.4 case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
17.5 }
17.6
17.7 + val popup: Markup_Tree.Select[XML.Tree] =
17.8 + {
17.9 + case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
17.10 + if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg
17.11 + }
17.12 +
17.13 val gutter_message: Markup_Tree.Select[Icon] =
17.14 {
17.15 case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
18.1 --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed Sep 29 11:55:08 2010 +0200
18.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed Sep 29 17:59:20 2010 +0200
18.3 @@ -9,12 +9,15 @@
18.4
18.5 import javax.swing.JSpinner
18.6
18.7 +import scala.swing.CheckBox
18.8 +
18.9 import org.gjt.sp.jedit.AbstractOptionPane
18.10
18.11
18.12 class Isabelle_Options extends AbstractOptionPane("isabelle")
18.13 {
18.14 private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
18.15 + private val auto_start = new CheckBox()
18.16 private val relative_font_size = new JSpinner()
18.17 private val tooltip_font_size = new JSpinner()
18.18 private val tooltip_dismiss_delay = new JSpinner()
18.19 @@ -23,26 +26,24 @@
18.20 {
18.21 addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
18.22
18.23 - addComponent(Isabelle.Property("relative-font-size.title"), {
18.24 - relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
18.25 - relative_font_size
18.26 - })
18.27 + addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
18.28 + auto_start.selected = Isabelle.Boolean_Property("auto-start")
18.29
18.30 - addComponent(Isabelle.Property("tooltip-font-size.title"), {
18.31 - tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
18.32 - tooltip_font_size
18.33 - })
18.34 + relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
18.35 + addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
18.36
18.37 - addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), {
18.38 - tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
18.39 - tooltip_dismiss_delay
18.40 - })
18.41 + tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
18.42 + addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
18.43 +
18.44 + tooltip_dismiss_delay.setValue(Isabelle.Int_Property("tooltip-dismiss-delay", 8000))
18.45 + addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
18.46 }
18.47
18.48 override def _save()
18.49 {
18.50 - Isabelle.Property("logic") =
18.51 - logic_selector.selection.item.name
18.52 + Isabelle.Property("logic") = logic_selector.selection.item.name
18.53 +
18.54 + Isabelle.Boolean_Property("auto-start") = auto_start.selected
18.55
18.56 Isabelle.Int_Property("relative-font-size") =
18.57 relative_font_size.getValue().asInstanceOf[Int]
19.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 29 11:55:08 2010 +0200
19.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 29 17:59:20 2010 +0200
19.3 @@ -223,34 +223,29 @@
19.4 {
19.5 /* session management */
19.6
19.7 - private def init_model(buffer: Buffer): Option[Document_Model] =
19.8 - {
19.9 - Document_Model(buffer) match {
19.10 - case Some(model) => model.refresh; Some(model)
19.11 - case None =>
19.12 - Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
19.13 - case Some((_, thy_name)) =>
19.14 - Some(Document_Model.init(Isabelle.session, buffer, thy_name))
19.15 - case None => None
19.16 - }
19.17 - }
19.18 - }
19.19 -
19.20 - private def activate_buffer(buffer: Buffer)
19.21 + private def init_model(buffer: Buffer)
19.22 {
19.23 Isabelle.swing_buffer_lock(buffer) {
19.24 - init_model(buffer) match {
19.25 - case None =>
19.26 - case Some(model) =>
19.27 - for (text_area <- Isabelle.jedit_text_areas(buffer)) {
19.28 - if (Document_View(text_area).map(_.model) != Some(model))
19.29 - Document_View.init(model, text_area)
19.30 - }
19.31 + val opt_model =
19.32 + Document_Model(buffer) match {
19.33 + case Some(model) => model.refresh; Some(model)
19.34 + case None =>
19.35 + Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
19.36 + case Some((_, thy_name)) =>
19.37 + Some(Document_Model.init(Isabelle.session, buffer, thy_name))
19.38 + case None => None
19.39 + }
19.40 + }
19.41 + if (opt_model.isDefined) {
19.42 + for (text_area <- Isabelle.jedit_text_areas(buffer)) {
19.43 + if (Document_View(text_area).map(_.model) != opt_model)
19.44 + Document_View.init(opt_model.get, text_area)
19.45 + }
19.46 }
19.47 }
19.48 }
19.49
19.50 - private def deactivate_buffer(buffer: Buffer)
19.51 + private def exit_model(buffer: Buffer)
19.52 {
19.53 Isabelle.swing_buffer_lock(buffer) {
19.54 Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
19.55 @@ -258,17 +253,52 @@
19.56 }
19.57 }
19.58
19.59 + private case class Init_Model(buffer: Buffer)
19.60 + private case class Exit_Model(buffer: Buffer)
19.61 + private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
19.62 + private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
19.63 +
19.64 private val session_manager = actor {
19.65 + var ready = false
19.66 loop {
19.67 react {
19.68 - case Session.Failed =>
19.69 - val text = new scala.swing.TextArea(Isabelle.session.syslog())
19.70 - text.editable = false
19.71 - Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
19.72 + case phase: Session.Phase =>
19.73 + ready = phase == Session.Ready
19.74 + phase match {
19.75 + case Session.Failed =>
19.76 + Swing_Thread.now {
19.77 + val text = new scala.swing.TextArea(Isabelle.session.syslog())
19.78 + text.editable = false
19.79 + Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
19.80 + }
19.81
19.82 - case Session.Ready => Isabelle.jedit_buffers.foreach(activate_buffer)
19.83 - case Session.Shutdown => Isabelle.jedit_buffers.foreach(deactivate_buffer)
19.84 - case _ =>
19.85 + case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
19.86 + case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
19.87 + case _ =>
19.88 + }
19.89 +
19.90 + case Init_Model(buffer) =>
19.91 + if (ready) init_model(buffer)
19.92 +
19.93 + case Exit_Model(buffer) =>
19.94 + exit_model(buffer)
19.95 +
19.96 + case Init_View(buffer, text_area) =>
19.97 + if (ready) {
19.98 + Isabelle.swing_buffer_lock(buffer) {
19.99 + Document_Model(buffer) match {
19.100 + case Some(model) => Document_View.init(model, text_area)
19.101 + case None =>
19.102 + }
19.103 + }
19.104 + }
19.105 +
19.106 + case Exit_View(buffer, text_area) =>
19.107 + Isabelle.swing_buffer_lock(buffer) {
19.108 + Document_View.exit(text_area)
19.109 + }
19.110 +
19.111 + case bad => System.err.println("session_manager: ignoring bad message " + bad)
19.112 }
19.113 }
19.114 }
19.115 @@ -283,15 +313,13 @@
19.116 if Isabelle.Boolean_Property("auto-start") => Isabelle.start_session()
19.117
19.118 case msg: BufferUpdate
19.119 - if Isabelle.session.phase == Session.Ready && // FIXME race!?
19.120 - msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
19.121 + if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
19.122
19.123 val buffer = msg.getBuffer
19.124 - if (buffer != null) activate_buffer(buffer)
19.125 + if (buffer != null) session_manager ! Init_Model(buffer)
19.126
19.127 case msg: EditPaneUpdate
19.128 - if Isabelle.session.phase == Session.Ready && // FIXME race!?
19.129 - (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
19.130 + if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
19.131 msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
19.132 msg.getWhat == EditPaneUpdate.CREATED ||
19.133 msg.getWhat == EditPaneUpdate.DESTROYED) =>
19.134 @@ -301,18 +329,11 @@
19.135 val text_area = edit_pane.getTextArea
19.136
19.137 if (buffer != null && text_area != null) {
19.138 - Isabelle.swing_buffer_lock(buffer) {
19.139 - msg.getWhat match {
19.140 - case EditPaneUpdate.BUFFER_CHANGING | EditPaneUpdate.DESTROYED =>
19.141 - Document_View.exit(text_area)
19.142 - case EditPaneUpdate.BUFFER_CHANGED | EditPaneUpdate.CREATED =>
19.143 - Document_Model(buffer) match {
19.144 - case Some(model) => Document_View.init(model, text_area)
19.145 - case None =>
19.146 - }
19.147 - case _ =>
19.148 - }
19.149 - }
19.150 + if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
19.151 + msg.getWhat == EditPaneUpdate.CREATED)
19.152 + session_manager ! Init_View(buffer, text_area)
19.153 + else
19.154 + session_manager ! Exit_View(buffer, text_area)
19.155 }
19.156
19.157 case msg: PropertiesChanged =>
20.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 29 11:55:08 2010 +0200
20.2 +++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Sep 29 17:59:20 2010 +0200
20.3 @@ -10,8 +10,7 @@
20.4 import isabelle._
20.5
20.6 import scala.actors.Actor._
20.7 -import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
20.8 - Component, Swing, CheckBox}
20.9 +import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
20.10 import scala.swing.event.{ButtonClicked, SelectionChanged}
20.11
20.12 import java.awt.BorderLayout
20.13 @@ -24,7 +23,7 @@
20.14 {
20.15 /* main tabs */
20.16
20.17 - private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 12)
20.18 + private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
20.19 readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
20.20
20.21 private val syslog = new TextArea(Isabelle.session.syslog())
20.22 @@ -55,14 +54,10 @@
20.23 session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
20.24 session_phase.tooltip = "Prover status"
20.25
20.26 - private val auto_start = new CheckBox("Auto start") {
20.27 - selected = Isabelle.Boolean_Property("auto-start")
20.28 - reactions += {
20.29 - case ButtonClicked(_) =>
20.30 - Isabelle.Boolean_Property("auto-start") = selected
20.31 - if (selected) Isabelle.start_session()
20.32 - }
20.33 + private val interrupt = new Button("Interrupt") {
20.34 + reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
20.35 }
20.36 + interrupt.tooltip = "Broadcast interrupt to all prover tasks"
20.37
20.38 private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
20.39 logic.listenTo(logic.selection)
20.40 @@ -70,13 +65,8 @@
20.41 case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
20.42 }
20.43
20.44 - private val interrupt = new Button("Interrupt") {
20.45 - reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
20.46 - }
20.47 - interrupt.tooltip = "Broadcast interrupt to all prover tasks"
20.48 -
20.49 private val controls =
20.50 - new FlowPanel(FlowPanel.Alignment.Right)(session_phase, auto_start, logic, interrupt)
20.51 + new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
20.52 add(controls.peer, BorderLayout.NORTH)
20.53
20.54