# HG changeset patch # User wenzelm # Date 1386264328 -3600 # Node ID 4ae29b8b1b8137a91f74e583abb893795d26486d # Parent cc126144f662a4de8f517947885252b576323dd5# Parent 748778ac0ab869c4b454e9bab3a6f000f12406ae merged diff -r cc126144f662 -r 4ae29b8b1b81 .hgtags --- a/.hgtags Thu Dec 05 17:09:13 2013 +0000 +++ b/.hgtags Thu Dec 05 18:25:28 2013 +0100 @@ -27,3 +27,4 @@ 21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012 d90218288d517942cfbc80a6b2654ecb22735e5c Isabelle2013 9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1 +4dd08fe126bad63aa05741d55fb3e86a2dbfc795 Isabelle2013-2 diff -r cc126144f662 -r 4ae29b8b1b81 ANNOUNCE --- a/ANNOUNCE Thu Dec 05 17:09:13 2013 +0000 +++ b/ANNOUNCE Thu Dec 05 18:25:28 2013 +0100 @@ -1,11 +1,11 @@ -Subject: Announcing Isabelle2013-1 +Subject: Announcing Isabelle2013-2 To: isabelle-users@cl.cam.ac.uk -Isabelle2013-1 is now available. +Isabelle2013-2 is now available. -This version consolidates Isabelle2013 and introduces numerous -improvements, see the NEWS file in the distribution for more details. -Some highlights are: +This version supersedes Isabelle2013-1, which in turn consolidated +Isabelle2013 and introduced numerous improvements. See the NEWS file +in the distribution for more details. Some highlights are: * Significantly improved Isabelle/jEdit Prover IDE. @@ -24,7 +24,7 @@ * HOL-BNF: significantly improved BNF-based (co)datatype package. -You may get Isabelle2013-1 from the following mirror sites: +You may get Isabelle2013-2 from the following mirror sites: Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/ Munich (Germany) http://isabelle.in.tum.de/ diff -r cc126144f662 -r 4ae29b8b1b81 Admin/Windows/Cygwin/README --- a/Admin/Windows/Cygwin/README Thu Dec 05 17:09:13 2013 +0000 +++ b/Admin/Windows/Cygwin/README Thu Dec 05 18:25:28 2013 +0100 @@ -9,7 +9,7 @@ * Local snapshots: http://isabelle.in.tum.de/cygwin (Isabelle2012) http://isabelle.in.tum.de/cygwin_2013 (Isabelle2013) - http://isabelle.in.tum.de/cygwin_2013-1 (Isabelle2013-1) + http://isabelle.in.tum.de/cygwin_2013-1 (Isabelle2013-1 and Isabelle2013-2) * Quasi-component: "isabelle makedist_cygwin" diff -r cc126144f662 -r 4ae29b8b1b81 Admin/Windows/WinRun4J/README --- a/Admin/Windows/WinRun4J/README Thu Dec 05 17:09:13 2013 +0000 +++ b/Admin/Windows/WinRun4J/README Thu Dec 05 18:25:28 2013 +0100 @@ -5,5 +5,5 @@ cp winrun4j/bin/WinRun4J.exe Isabelle.exe winrun4j/bin/RCEDIT /C Isabelle.exe -winrun4j/bin/RCEDIT /I Isabelle.exe isabelle.ico +winrun4j/bin/RCEDIT /I Isabelle.exe isabelle_transparent.ico diff -r cc126144f662 -r 4ae29b8b1b81 Admin/Windows/WinRun4J/isabelle.ico Binary file Admin/Windows/WinRun4J/isabelle.ico has changed diff -r cc126144f662 -r 4ae29b8b1b81 Admin/Windows/WinRun4J/isabelle_transparent.ico Binary file Admin/Windows/WinRun4J/isabelle_transparent.ico has changed diff -r cc126144f662 -r 4ae29b8b1b81 Admin/components/bundled-windows --- a/Admin/components/bundled-windows Thu Dec 05 17:09:13 2013 +0000 +++ b/Admin/components/bundled-windows Thu Dec 05 18:25:28 2013 +0100 @@ -1,3 +1,3 @@ #additional components to be bundled for release cygwin-20130916 -windows_app-20130909 +windows_app-20131201 diff -r cc126144f662 -r 4ae29b8b1b81 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Dec 05 17:09:13 2013 +0000 +++ b/Admin/components/components.sha1 Thu Dec 05 18:25:28 2013 +0100 @@ -70,6 +70,8 @@ e6a43b7b3b21295853bd2a63b27ea20bd6102f5f windows_app-20130906.tar.gz 8fe004aead867d4c82425afac481142bd3f01fb0 windows_app-20130908.tar.gz d273abdc7387462f77a127fa43095eed78332b5c windows_app-20130909.tar.gz +c368908584e2bca38b3bcb20431d0c69399fc2f0 windows_app-20131130.tar.gz +c3f5285481a95fde3c1961595b4dd0311ee7ac1f windows_app-20131201.tar.gz 1c36a840320dfa9bac8af25fc289a4df5ea3eccb xz-java-1.2-1.tar.gz 2ae13aa17d0dc95ce254a52f1dba10929763a10d xz-java-1.2.tar.gz 4530a1aa6f4498ee3d78d6000fa71a3f63bd077f yices-1.0.28.tar.gz diff -r cc126144f662 -r 4ae29b8b1b81 Admin/lib/Tools/makedist_bundle --- a/Admin/lib/Tools/makedist_bundle Thu Dec 05 17:09:13 2013 +0000 +++ b/Admin/lib/Tools/makedist_bundle Thu Dec 05 18:25:28 2013 +0100 @@ -147,6 +147,9 @@ # platform-specific setup (inside archive) +perl -pi -e "s,view.title=Isabelle/jEdit,view.title=${ISABELLE_NAME},g;" \ + "$ISABELLE_TARGET/src/Tools/jEdit/dist/properties/jEdit.props" + case "$PLATFORM_FAMILY" in linux) purge_contrib '-name "x86*-darwin" -o -name "x86*-cygwin" -o -name "x86*-windows"' diff -r cc126144f662 -r 4ae29b8b1b81 NEWS --- a/NEWS Thu Dec 05 17:09:13 2013 +0000 +++ b/NEWS Thu Dec 05 18:25:28 2013 +0100 @@ -84,6 +84,11 @@ shows up as additional case in fixpoint induction proofs. INCOMPATIBILITY +* Nitpick: + - Fixed soundness bug whereby mutually recursive datatypes could take + infinite values. + + *** ML *** * Toplevel function "use" refers to raw ML bootstrap environment, @@ -93,6 +98,35 @@ +New in Isabelle2013-2 (December 2013) +------------------------------------- + +*** Prover IDE -- Isabelle/Scala/jEdit *** + +* More robust editing of running commands with internal forks, +e.g. non-terminating 'by' steps. + +* More relaxed Sledgehammer panel: avoid repeated application of query +after edits surrounding the command location. + +* More status information about commands that are interrupted +accidentally (via physical event or Poly/ML runtime system signal, +e.g. out-of-memory). + + +*** System *** + +* More robust termination of external processes managed by +Isabelle/ML: support cancellation of tasks within the range of +milliseconds, as required for PIDE document editing with automatically +tried tools (e.g. Sledgehammer). + +* Reactivated Isabelle/Scala kill command for external processes on +Mac OS X, which was accidentally broken in Isabelle2013-1 due to a +workaround for some Debian/Ubuntu Linux versions from 2013. + + + New in Isabelle2013-1 (November 2013) ------------------------------------- @@ -520,10 +554,6 @@ sets ~> set IMCOMPATIBILITY. -* Nitpick: - - Fixed soundness bug whereby mutually recursive datatypes could take - infinite values. - *** ML *** diff -r cc126144f662 -r 4ae29b8b1b81 lib/logo/isabelle-16.gif Binary file lib/logo/isabelle-16.gif has changed diff -r cc126144f662 -r 4ae29b8b1b81 lib/logo/isabelle-24.gif Binary file lib/logo/isabelle-24.gif has changed diff -r cc126144f662 -r 4ae29b8b1b81 lib/logo/isabelle-32.gif Binary file lib/logo/isabelle-32.gif has changed diff -r cc126144f662 -r 4ae29b8b1b81 lib/logo/isabelle-48.gif Binary file lib/logo/isabelle-48.gif has changed diff -r cc126144f662 -r 4ae29b8b1b81 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Doc/JEdit/JEdit.thy Thu Dec 05 18:25:28 2013 +0100 @@ -121,9 +121,12 @@ subsection {* Documentation *} text {* Regular jEdit documentation is accessible via its @{verbatim - Help} menu or @{verbatim F1} keyboard shortcut. This includes a full - \emph{User's Guide} and \emph{Frequently Asked Questions} for this - sophisticated text editor. + Help} menu or @{verbatim F1} keyboard shortcut. This includes a + full \emph{User's Guide} and \emph{Frequently Asked Questions} for + this sophisticated text editor. The same can be browsed without the + technical restrictions of the built-in Java HTML viewer here: + \url{http://www.jedit.org/index.php?page=docs} (potentially for a + different version of jEdit). Most of this information about jEdit is relevant for Isabelle/jEdit as well, but one needs to keep in mind that defaults sometimes @@ -227,7 +230,8 @@ theme is selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was once marketed aggressively by Sun, but never quite finished, and is today (2013) lagging a bit behind further - development of Swing and GTK.} + development of Swing and GTK. The graphics rendering performance + can be worse than for other Swing look-and-feels.} \item[Windows] Regular \emph{Windows} is used by default, but \emph{Windows Classic} also works. @@ -477,7 +481,7 @@ \medskip A black rectangle in the text indicates a hyperlink that may be followed by a mouse click (while the @{verbatim CONTROL} or @{verbatim COMMAND} modifier key is still pressed). Presently - (Isabelle2013-1) there is no systematic navigation within the + (Isabelle2013-2) there is no systematic navigation within the editor to return to the original location. Also note that the link target may be a file that is itself not @@ -1103,7 +1107,7 @@ \textbf{Workaround:} Do not use input methods, reset the environment variable @{verbatim XMODIFIERS} within Isabelle settings (default in - Isabelle2013-1). + Isabelle2013-2). \item \textbf{Problem:} Some Linux / X11 window managers that are not ``re-parenting'' cause problems with additional windows opened diff -r cc126144f662 -r 4ae29b8b1b81 src/Doc/Tutorial/Types/Overloading.thy --- a/src/Doc/Tutorial/Types/Overloading.thy Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Doc/Tutorial/Types/Overloading.thy Thu Dec 05 18:25:28 2013 +0100 @@ -7,7 +7,7 @@ subsubsection {* Overloading *} -text {* We can introduce a binary infix addition operator @{text "\"} +text {* We can introduce a binary infix addition operator @{text "\"} for arbitrary types by means of a type class: *} class plus = diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/Concurrent/bash.ML Thu Dec 05 18:25:28 2013 +0100 @@ -23,6 +23,13 @@ val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); + fun cleanup_files () = + (try File.rm script_path; + try File.rm out_path; + try File.rm err_path; + try File.rm pid_path); + val _ = cleanup_files (); + val system_thread = Simple_Thread.fork false (fn () => Multithreading.with_attributes Multithreading.private_interrupts (fn _ => @@ -55,37 +62,36 @@ handle exn => (Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); - fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE; + fun read_pid 0 = NONE + | read_pid count = + (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of + NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) + | some => some); - fun terminate opt_pid = - let - val sig_test = Posix.Signal.fromWord 0w0; - - fun kill_group pid s = - (Posix.Process.kill - (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) - handle OS.SysErr _ => false; + fun terminate NONE = () + | terminate (SOME pid) = + let + val sig_test = Posix.Signal.fromWord 0w0; - fun kill s = - (case opt_pid of - NONE => true - | SOME pid => (kill_group pid s; kill_group pid sig_test)); + fun kill_group pid s = + (Posix.Process.kill + (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) + handle OS.SysErr _ => false; + + fun kill s = (kill_group pid s; kill_group pid sig_test); - fun multi_kill count s = - count = 0 orelse - kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); - val _ = - multi_kill 10 Posix.Signal.int andalso - multi_kill 10 Posix.Signal.term andalso - multi_kill 10 Posix.Signal.kill; - in () end; + fun multi_kill count s = + count = 0 orelse + kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); + val _ = + multi_kill 10 Posix.Signal.int andalso + multi_kill 10 Posix.Signal.term andalso + multi_kill 10 Posix.Signal.kill; + in () end; fun cleanup () = (Simple_Thread.interrupt_unsynchronized system_thread; - try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); + cleanup_files ()); in let val _ = @@ -95,10 +101,10 @@ val out = the_default "" (try File.read out_path); val err = the_default "" (try File.read err_path); val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = get_pid (); + val pid = read_pid 1; val _ = cleanup (); in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (get_pid ()); cleanup (); reraise exn) + handle exn => (terminate (read_pid 10); cleanup (); reraise exn) end); end; diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/Concurrent/future.ML --- a/src/Pure/Concurrent/future.ML Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/Concurrent/future.ML Thu Dec 05 18:25:28 2013 +0100 @@ -48,8 +48,6 @@ val worker_group: unit -> group option val the_worker_group: unit -> group val worker_subgroup: unit -> group - val worker_nest: string -> ('a -> 'b) -> 'a -> 'b - val worker_guest: string -> group -> ('a -> 'b) -> 'a -> 'b type 'a future val task_of: 'a future -> task val peek: 'a future -> 'a Exn.result option @@ -69,6 +67,7 @@ val joins: 'a future list -> 'a list val join: 'a future -> 'a val join_tasks: task list -> unit + val task_context: string -> group -> ('a -> 'b) -> 'a -> 'b val value_result: 'a Exn.result -> 'a future val value: 'a -> 'a future val cond_forks: params -> (unit -> 'a) list -> 'a future list @@ -110,14 +109,6 @@ fun worker_subgroup () = new_group (worker_group ()); -fun worker_nest name f x = - setmp_worker_task (Task_Queue.new_task (the_worker_group ()) name NONE) f x; - -fun worker_guest name group f x = - if is_some (worker_task ()) then - raise Fail "Already running as worker thread" - else setmp_worker_task (Task_Queue.new_task group name NONE) f x; - fun worker_joining e = (case worker_task () of NONE => e () @@ -477,7 +468,7 @@ (* future jobs *) -fun future_job group interrupts (e: unit -> 'a) = +fun future_job group atts (e: unit -> 'a) = let val result = Single_Assignment.var "future" : 'a result; val pos = Position.thread_data (); @@ -486,10 +477,7 @@ val res = if ok then Exn.capture (fn () => - Multithreading.with_attributes - (if interrupts - then Multithreading.private_interrupts else Multithreading.no_interrupts) - (fn _ => Position.setmp_thread_data pos e ())) () + Multithreading.with_attributes atts (fn _ => Position.setmp_thread_data pos e ())) () else Exn.interrupt_exn; in assign_result group result (identify_result pos res) end; in (result, job) end; @@ -510,7 +498,11 @@ | SOME grp => grp); fun enqueue e queue = let - val (result, job) = future_job grp interrupts e; + val atts = + if interrupts + then Multithreading.private_interrupts + else Multithreading.no_interrupts; + val (result, job) = future_job grp atts e; val (task, queue') = Task_Queue.enqueue name grp deps pri job queue; val future = Future {promised = false, task = task, result = result}; in (future, queue') end; @@ -586,6 +578,23 @@ |> join; +(* task context for running thread *) + +fun task_context name group f x = + Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts => + let + val (result, job) = future_job group orig_atts (fn () => f x); + val task = + SYNCHRONIZED "enroll" (fn () => + Unsynchronized.change_result queue (Task_Queue.enroll (Thread.self ()) name group)); + val _ = worker_exec (task, [job]); + in + (case Single_Assignment.peek result of + NONE => raise Fail "Missing task context result" + | SOME res => Exn.release res) + end); + + (* fast-path operations -- bypass task queue if possible *) fun value_result (res: 'a Exn.result) = @@ -608,7 +617,8 @@ let val task = task_of x; val group = Task_Queue.group_of_task task; - val (result, job) = future_job group true (fn () => f (join x)); + val (result, job) = + future_job group Multithreading.private_interrupts (fn () => f (join x)); val extended = SYNCHRONIZED "extend" (fn () => (case Task_Queue.extend task job (! queue) of diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/Concurrent/task_queue.ML --- a/src/Pure/Concurrent/task_queue.ML Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/Concurrent/task_queue.ML Thu Dec 05 18:25:28 2013 +0100 @@ -17,7 +17,6 @@ val str_of_groups: group -> string type task val dummy_task: task - val new_task: group -> string -> int option -> task val group_of_task: task -> group val name_of_task: task -> string val pri_of_task: task -> int @@ -36,6 +35,7 @@ val cancel: queue -> group -> Thread.thread list val cancel_all: queue -> group list * Thread.thread list val finish: task -> queue -> bool * queue + val enroll: Thread.thread -> string -> group -> queue -> task * queue val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue val extend: task -> (bool -> bool) -> queue -> queue option @@ -295,6 +295,16 @@ in (maximal, make_queue groups' jobs') end; +(* enroll *) + +fun enroll thread name group (Queue {groups, jobs}) = + let + val task = new_task group name NONE; + val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups; + val jobs' = jobs |> Task_Graph.new_node (task, Running thread); + in (task, make_queue groups' jobs') end; + + (* enqueue *) fun enqueue_passive group abort (Queue {groups, jobs}) = diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/GUI/gui.scala Thu Dec 05 18:25:28 2013 +0100 @@ -127,7 +127,7 @@ /* icon */ def isabelle_icon(): ImageIcon = - new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle.gif")) + new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle-32.gif")) def isabelle_image(): Image = isabelle_icon().getImage diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/PIDE/command.ML Thu Dec 05 18:25:28 2013 +0100 @@ -59,15 +59,17 @@ (case expr of Expr (exec_id, body) => uninterruptible (fn restore_attributes => fn () => - if Execution.running execution_id exec_id [Future.the_worker_group ()] then - let - val res = - (body - |> restore_attributes - |> Future.worker_nest "Command.memo_exec" - |> Exn.interruptible_capture) (); - in SOME ((), Result res) end - else SOME ((), expr)) () + let val group = Future.worker_subgroup () in + if Execution.running execution_id exec_id [group] then + let + val res = + (body + |> restore_attributes + |> Future.task_context "Command.memo_exec" group + |> Exn.interruptible_capture) (); + in SOME ((), Result res) end + else SOME ((), expr) + end) () | Result _ => SOME ((), expr))) |> (fn NONE => error "Conflicting command execution" | _ => ()); @@ -196,18 +198,19 @@ val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); val errs = errs1 @ errs2; - val _ = Toplevel.status tr Markup.finished; val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; in (case result of NONE => let + val _ = Toplevel.status tr Markup.failed; + val _ = Toplevel.status tr Markup.finished; val _ = if null errs then Exn.interrupt () else (); - val _ = Toplevel.status tr Markup.failed; in {failed = true, malformed = malformed', command = tr, state = st} end | SOME st' => let val _ = proof_status tr st'; + val _ = Toplevel.status tr Markup.finished; in {failed = false, malformed = malformed', command = tr, state = st'} end) end; diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/PIDE/execution.ML --- a/src/Pure/PIDE/execution.ML Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/PIDE/execution.ML Thu Dec 05 18:25:28 2013 +0100 @@ -104,17 +104,18 @@ val result = Exn.capture (Future.interruptible_task e) () |> Future.identify_result pos; - val _ = status task [Markup.finished, Markup.joined]; + val _ = status task [Markup.joined]; val _ = (case result of Exn.Res _ => () | Exn.Exn exn => - if exec_id = 0 orelse Exn.is_interrupt exn then () - else - (status task [Markup.failed]; - Output.report (Markup.markup_only Markup.bad); - List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))); + (status task [Markup.failed]; + Output.report (Markup.markup_only Markup.bad); + if exec_id = 0 then () + else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))); + val _ = status task [Markup.finished]; in Exn.release result end); + val _ = status (Future.task_of future) [Markup.forked]; in future end)) (); diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/PIDE/query_operation.scala --- a/src/Pure/PIDE/query_operation.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/PIDE/query_operation.scala Thu Dec 05 18:25:28 2013 +0100 @@ -18,7 +18,6 @@ val WAITING = Value("waiting") val RUNNING = Value("running") val FINISHED = Value("finished") - val REMOVED = Value("removed") } } @@ -38,7 +37,7 @@ private var current_query: List[String] = Nil private var current_update_pending = false private var current_output: List[XML.Tree] = Nil - private var current_status = Query_Operation.Status.REMOVED + private var current_status = Query_Operation.Status.FINISHED private var current_exec_id = Document_ID.none private def reset_state() @@ -47,7 +46,7 @@ current_query = Nil current_update_pending = false current_output = Nil - current_status = Query_Operation.Status.REMOVED + current_status = Query_Operation.Status.FINISHED current_exec_id = Document_ID.none } @@ -89,13 +88,40 @@ } yield elem).toList + /* resolve sendback: static command id */ + + def resolve_sendback(body: XML.Body): XML.Body = + { + current_location match { + case None => body + case Some(command) => + def resolve(body: XML.Body): XML.Body = + body map { + case XML.Wrapped_Elem(m, b1, b2) => XML.Wrapped_Elem(m, resolve(b1), resolve(b2)) + case XML.Elem(Markup(Markup.SENDBACK, props), b) => + val props1 = + props.map({ + case (Markup.ID, Properties.Value.Long(id)) if id == current_exec_id => + (Markup.ID, Properties.Value.Long(command.id)) + case p => p + }) + XML.Elem(Markup(Markup.SENDBACK, props1), resolve(b)) + case XML.Elem(m, b) => XML.Elem(m, resolve(b)) + case t => t + } + resolve(body) + } + } + + /* output */ val new_output = for { XML.Elem(_, List(XML.Elem(markup, body))) <- results if Markup.messages.contains(markup.name) - } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) + body1 = resolve_sendback(body) + } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body1) /* status */ @@ -105,7 +131,7 @@ results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) val new_status = - if (removed) Query_Operation.Status.REMOVED + if (removed) Query_Operation.Status.FINISHED else get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse @@ -133,7 +159,7 @@ if (current_status != new_status) { current_status = new_status consume_status(new_status) - if (new_status == Query_Operation.Status.REMOVED) + if (new_status == Query_Operation.Status.FINISHED) remove_overlay() } } @@ -192,7 +218,7 @@ current_location match { case Some(command) if current_update_pending || - (current_status != Query_Operation.Status.REMOVED && + (current_status != Query_Operation.Status.FINISHED && changed.commands.contains(command)) => Swing_Thread.later { content_update() } case _ => diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/System/isabelle_process.ML Thu Dec 05 18:25:28 2013 +0100 @@ -159,8 +159,8 @@ NONE => raise Runtime.TERMINATE | SOME line => map (read_chunk channel) (space_explode "," line)); -fun worker_guest e = - Future.worker_guest "Isabelle_Process.loop" (Future.new_group NONE) e (); +fun task_context e = + Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e (); in @@ -168,7 +168,7 @@ let val continue = (case read_command channel of [] => (Output.error_message "Isabelle process: no input"; true) - | name :: args => (worker_guest (fn () => run_command name args); true)) + | name :: args => (task_context (fn () => run_command name args); true)) handle Runtime.TERMINATE => false | exn => (ML_Compiler.exn_error_message exn handle crash => recover crash; true); in diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/System/isabelle_system.scala Thu Dec 05 18:25:28 2013 +0100 @@ -302,11 +302,14 @@ private val pid = stdout.readLine + private def kill_cmd(signal: String): Int = + execute(true, "/bin/bash", "-c", "kill -" + signal + " -" + pid).waitFor + private def kill(signal: String): Boolean = { try { - execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor - execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0 + kill_cmd(signal) + kill_cmd("0") == 0 } catch { case _: InterruptedException => true } } diff -r cc126144f662 -r 4ae29b8b1b81 src/Pure/build-jars --- a/src/Pure/build-jars Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Pure/build-jars Thu Dec 05 18:25:28 2013 +0100 @@ -220,7 +220,7 @@ mkdir -p "$(dirname "$CHARSET_SERVICE")" echo isabelle.Isabelle_Charset_Provider > "$CHARSET_SERVICE" - cp "$ISABELLE_HOME/lib/logo/isabelle.gif" isabelle/. + cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" isabelle/. isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.Main META-INF isabelle || \ fail "Failed to produce $TARGET" diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Dec 05 18:25:28 2013 +0100 @@ -280,6 +280,16 @@ print qq,\n\n,; } print; }' dist/modes/catalog + cd dist + isabelle_jdk jar xf jedit.jar + cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \ + "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed + cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \ + "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed + isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed + rm -rf META-INF org + cd .. + cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed ( #workaround for scalac 2.10.2 diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/src/active.scala Thu Dec 05 18:25:28 2013 +0100 @@ -52,9 +52,9 @@ case XML.Elem(Markup(Markup.SENDBACK, props), _) => props match { - case Position.Id(exec_id) => + case Position.Id(id) => Isabelle.edit_command(snapshot, buffer, - props.exists(_ == Markup.PADDING_COMMAND), exec_id, text) + props.exists(_ == Markup.PADDING_COMMAND), id, text) case _ => if (props.exists(_ == Markup.PADDING_LINE)) Isabelle.insert_line_padding(text_area, text) diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/src/find_dockable.scala Thu Dec 05 18:25:28 2013 +0100 @@ -37,7 +37,7 @@ process_indicator.update("Waiting for evaluation of context ...", 5) case Query_Operation.Status.RUNNING => process_indicator.update("Running find operation ...", 15) - case _ => + case Query_Operation.Status.FINISHED => process_indicator.update(null, 0) } } diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/src/isabelle.scala Thu Dec 05 18:25:28 2013 +0100 @@ -177,26 +177,28 @@ snapshot: Document.Snapshot, buffer: Buffer, padding: Boolean, - exec_id: Document_ID.Exec, + id: Document_ID.Generic, s: String) { - snapshot.state.execs.get(exec_id).map(_.command) match { - case Some(command) => - snapshot.node.command_start(command) match { - case Some(start) => - JEdit_Lib.buffer_edit(buffer) { - val range = command.proper_range + start - if (padding) { - buffer.insert(start + range.length, "\n" + s) + if (!snapshot.is_outdated) { + snapshot.state.find_command(snapshot.version, id) match { + case Some((node, command)) => + node.command_start(command) match { + case Some(start) => + JEdit_Lib.buffer_edit(buffer) { + val range = command.proper_range + start + if (padding) { + buffer.insert(start + range.length, "\n" + s) + } + else { + buffer.remove(start, range.length) + buffer.insert(start, s) + } } - else { - buffer.remove(start, range.length) - buffer.insert(start, s) - } - } - case None => - } - case None => + case None => + } + case None => + } } } diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/src/jEdit.props Thu Dec 05 18:25:28 2013 +0100 @@ -223,6 +223,7 @@ largefilemode=full line-end.shortcut=END line-home.shortcut=HOME +logo.icon.medium=32x32/apps/isabelle.gif lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel match-bracket.shortcut2=C+9 next-bracket.shortcut2=C+e C+9 @@ -264,4 +265,5 @@ view.middleMousePaste=true view.showToolbar=false view.thickCaret=true +view.title=Isabelle/jEdit -\u0020 view.width=1072 diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 05 18:25:28 2013 +0100 @@ -38,7 +38,7 @@ process_indicator.update("Waiting for evaluation of context ...", 5) case Query_Operation.Status.RUNNING => process_indicator.update("Sledgehammering ...", 15) - case _ => + case Query_Operation.Status.FINISHED => process_indicator.update(null, 0) } } diff -r cc126144f662 -r 4ae29b8b1b81 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Thu Dec 05 17:09:13 2013 +0000 +++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Dec 05 18:25:28 2013 +0100 @@ -74,6 +74,7 @@ } private val continuous_checking = new Isabelle.Continuous_Checking + continuous_checking.focusable = false private val logic = Isabelle_Logic.logic_selector(true)