--- a/.hgtags Mon Nov 11 17:34:44 2013 +0100
+++ b/.hgtags Thu Dec 05 17:51:29 2013 +0100
@@ -27,3 +27,7 @@
21c42b095c841d1a7508c143d6b6e98d95dbfa69 Isabelle2012
d90218288d517942cfbc80a6b2654ecb22735e5c Isabelle2013
9c1f2136532626c7cb5fae14a2aeac53be3aeb67 Isabelle2013-1
+57aefb80b639c59bc85347500b9b2f9ef9cc14c6 Isabelle2013-2-RC1
+99b9249b3e05c52f62ee6b479e723b44dfd0be77 Isabelle2013-2-RC2
+aeb21314d0788414371c41ebbca32a0d0528108e Isabelle2013-2-RC3
+4dd08fe126bad63aa05741d55fb3e86a2dbfc795 Isabelle2013-2
--- a/ANNOUNCE Mon Nov 11 17:34:44 2013 +0100
+++ b/ANNOUNCE Thu Dec 05 17:51:29 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/
--- a/Admin/Windows/Cygwin/README Mon Nov 11 17:34:44 2013 +0100
+++ b/Admin/Windows/Cygwin/README Thu Dec 05 17:51:29 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"
--- a/Admin/Windows/WinRun4J/README Mon Nov 11 17:34:44 2013 +0100
+++ b/Admin/Windows/WinRun4J/README Thu Dec 05 17:51:29 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
Binary file Admin/Windows/WinRun4J/isabelle.ico has changed
Binary file Admin/Windows/WinRun4J/isabelle_transparent.ico has changed
--- a/Admin/components/bundled-windows Mon Nov 11 17:34:44 2013 +0100
+++ b/Admin/components/bundled-windows Thu Dec 05 17:51:29 2013 +0100
@@ -1,3 +1,3 @@
#additional components to be bundled for release
cygwin-20130916
-windows_app-20130909
+windows_app-20131201
--- a/Admin/components/components.sha1 Mon Nov 11 17:34:44 2013 +0100
+++ b/Admin/components/components.sha1 Thu Dec 05 17:51:29 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
--- a/Admin/lib/Tools/makedist_bundle Mon Nov 11 17:34:44 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundle Thu Dec 05 17:51:29 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"'--- a/NEWS Mon Nov 11 17:34:44 2013 +0100
+++ b/NEWS Thu Dec 05 17:51:29 2013 +0100
@@ -1,6 +1,35 @@
Isabelle NEWS -- history user-relevant changes
==============================================
+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)
-------------------------------------
Binary file lib/logo/isabelle-16.gif has changed
Binary file lib/logo/isabelle-24.gif has changed
Binary file lib/logo/isabelle-32.gif has changed
Binary file lib/logo/isabelle-48.gif has changed
--- a/src/Doc/JEdit/JEdit.thy Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy Thu Dec 05 17:51:29 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.
@@ -278,10 +282,9 @@
\emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
file-system access.} Moreover, environment variables from the
Isabelle process may be used freely, e.g.\ @{file
- "$ISABELLE_HOME/etc/symbols"} or @{file
- "$ISABELLE_JDK_HOME/README.html"}. There are special shortcuts:
- @{file "~"} for @{file "$USER_HOME"} and @{file "~~"} for @{file
- "$ISABELLE_HOME"}.
+ "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}.
+ There are special shortcuts: @{file "~"} for @{file "$USER_HOME"}
+ and @{file "~~"} for @{file "$ISABELLE_HOME"}.
\medskip Since jEdit happens to support environment variables within
file specifications as well, it is natural to use similar notation
@@ -478,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
@@ -1110,7 +1113,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--- a/src/Doc/Tutorial/Types/Overloading.thy Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Doc/Tutorial/Types/Overloading.thy Thu Dec 05 17:51:29 2013 +0100
@@ -7,7 +7,7 @@
subsubsection {* Overloading *}
-text {* We can introduce a binary infix addition operator @{text "\<otimes>"}
+text {* We can introduce a binary infix addition operator @{text "\<oplus>"}
for arbitrary types by means of a type class: *}
class plus =--- a/src/Pure/Concurrent/bash.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/Concurrent/bash.ML Thu Dec 05 17:51:29 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;--- a/src/Pure/Concurrent/future.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Dec 05 17:51:29 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--- a/src/Pure/Concurrent/task_queue.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/Concurrent/task_queue.ML Thu Dec 05 17:51:29 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}) =--- a/src/Pure/GUI/gui.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/GUI/gui.scala Thu Dec 05 17:51:29 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
--- a/src/Pure/PIDE/command.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/PIDE/command.ML Thu Dec 05 17:51:29 2013 +0100
@@ -57,15 +57,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" | _ => ());
@@ -163,18 +165,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;
--- a/src/Pure/PIDE/execution.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/PIDE/execution.ML Thu Dec 05 17:51:29 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)) ();
--- a/src/Pure/PIDE/query_operation.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/PIDE/query_operation.scala Thu Dec 05 17:51:29 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 _ =>--- a/src/Pure/System/isabelle_process.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/System/isabelle_process.ML Thu Dec 05 17:51:29 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_msg "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 => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
in--- a/src/Pure/System/isabelle_system.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Dec 05 17:51:29 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 }
}--- a/src/Pure/build-jars Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Pure/build-jars Thu Dec 05 17:51:29 2013 +0100
@@ -219,7 +219,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"--- a/src/Tools/adhoc_overloading.ML Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/adhoc_overloading.ML Thu Dec 05 17:51:29 2013 +0100
@@ -178,9 +178,9 @@
fun check ctxt =
map (fn t => Term.map_aterms (insert_variants ctxt t) t);
-fun uncheck ctxt =
- if Config.get ctxt show_variants then I
- else map (insert_overloaded ctxt);
+fun uncheck ctxt ts =
+ if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts
+ else map (insert_overloaded ctxt) ts;
fun reject_unresolved ctxt =
let
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Thu Dec 05 17:51:29 2013 +0100
@@ -280,6 +280,16 @@
print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\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--- a/src/Tools/jEdit/src/active.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/src/active.scala Thu Dec 05 17:51:29 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)--- a/src/Tools/jEdit/src/find_dockable.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Thu Dec 05 17:51:29 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)
}
}--- a/src/Tools/jEdit/src/isabelle.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Thu Dec 05 17:51:29 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 =>
+ }
}
}
--- a/src/Tools/jEdit/src/jEdit.props Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Thu Dec 05 17:51:29 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
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Dec 05 17:51:29 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)
}
}--- a/src/Tools/jEdit/src/theories_dockable.scala Mon Nov 11 17:34:44 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Dec 05 17:51:29 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)