--- a/.hgtags Mon Aug 18 14:09:21 2014 +0200
+++ b/.hgtags Mon Aug 18 14:19:23 2014 +0200
@@ -32,3 +32,4 @@
c0fd03d13d28954f6b7018f273b6edb17fcdeaf7 Isabelle2014-RC1
ee908fccabc220a5f2e5af533d13ebceeb0e09ff Isabelle2014-RC2
91e188508bc9df5de2737325c390836603a3e409 Isabelle2014-RC3
+113b43b84412416c67dc5e46f0d79473c837fbda Isabelle2014-RC4
--- a/Admin/components/bundled-windows Mon Aug 18 14:09:21 2014 +0200
+++ b/Admin/components/bundled-windows Mon Aug 18 14:19:23 2014 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20140725
+cygwin-20140813
windows_app-20131201
--- a/Admin/components/components.sha1 Mon Aug 18 14:09:21 2014 +0200
+++ b/Admin/components/components.sha1 Mon Aug 18 14:19:23 2014 +0200
@@ -9,6 +9,7 @@
acbc4bf161ad21e96ecfe506266ccdbd288f8a6f cygwin-20140530.tar.gz
3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41 cygwin-20140626.tar.gz
8e562dfe57a2f894f9461f4addedb88afa108152 cygwin-20140725.tar.gz
+238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf cygwin-20140813.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -29,6 +30,7 @@
dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c jdk-7u40.tar.gz
71b629b2ce83dbb69967c4785530afce1bec3809 jdk-7u60.tar.gz
e119f4cbfa2a39a53b9578d165d0dc44b59527b7 jdk-7u65.tar.gz
+d6d1c42989433839fe64f34eb77298ef6627aed4 jdk-7u67.tar.gz
ec740ee9ffd43551ddf1e5b91641405116af6291 jdk-7u6.tar.gz
7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
--- a/Admin/components/main Mon Aug 18 14:09:21 2014 +0200
+++ b/Admin/components/main Mon Aug 18 14:19:23 2014 +0200
@@ -3,7 +3,7 @@
e-1.8
exec_process-1.0.3
Haskabelle-2014
-jdk-7u65
+jdk-7u67
jedit_build-20140722
jfreechart-1.0.14-1
jortho-1.0-2
--- a/Admin/java/build Mon Aug 18 14:09:21 2014 +0200
+++ b/Admin/java/build Mon Aug 18 14:19:23 2014 +0200
@@ -11,8 +11,8 @@
## parameters
-VERSION="7u65"
-FULL_VERSION="1.7.0_65"
+VERSION="7u67"
+FULL_VERSION="1.7.0_67"
ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
--- a/etc/options Mon Aug 18 14:09:21 2014 +0200
+++ b/etc/options Mon Aug 18 14:19:23 2014 +0200
@@ -138,6 +138,9 @@
option editor_execution_delay : real = 0.02
-- "delay for start of execution process after document update (seconds)"
+option editor_syslog_limit : int = 100
+ -- "maximum amount of buffered syslog messages"
+
section "Miscellaneous Tools"
--- a/src/Doc/Isar_Ref/Proof.thy Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Aug 18 14:19:23 2014 +0200
@@ -520,10 +520,10 @@
\secref{sec:term-abbrev}.
The optional case names of @{element_ref "obtains"} have a twofold
- meaning: (1) during the of this claim they refer to the the local
- context introductions, (2) the resulting rule is annotated
- accordingly to support symbolic case splits when used with the
- @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
+ meaning: (1) in the proof of this claim they refer to the local context
+ introductions, (2) in the resulting rule they become annotations for
+ symbolic case splits, e.g.\ for the @{method_ref cases} method
+ (\secref{sec:cases-induct}).
*}
--- a/src/Pure/General/output.ML Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Pure/General/output.ML Mon Aug 18 14:19:23 2014 +0200
@@ -29,6 +29,7 @@
val urgent_message: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
+ val system_message: string -> unit
val prompt: string -> unit
val status: string -> unit
val report: string list -> unit
@@ -45,6 +46,7 @@
val tracing_fn: (output list -> unit) Unsynchronized.ref
val warning_fn: (output list -> unit) Unsynchronized.ref
val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
+ val system_message_fn: (output list -> unit) Unsynchronized.ref
val prompt_fn: (output -> unit) Unsynchronized.ref
val status_fn: (output list -> unit) Unsynchronized.ref
val report_fn: (output list -> unit) Unsynchronized.ref
@@ -101,6 +103,7 @@
val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
val error_message_fn =
Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
+val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
val prompt_fn = Unsynchronized.ref physical_stdout; (*Proof General legacy*)
val status_fn = Unsynchronized.ref (fn _: output list => ());
val report_fn = Unsynchronized.ref (fn _: output list => ());
@@ -115,6 +118,7 @@
fun warning s = ! warning_fn [output s];
fun error_message' (i, s) = ! error_message_fn (i, [output s]);
fun error_message s = error_message' (serial (), s);
+fun system_message s = ! system_message_fn [output s];
fun prompt s = ! prompt_fn (output s);
fun status s = ! status_fn [output s];
fun report ss = ! report_fn (map output ss);
--- a/src/Pure/Isar/runtime.ML Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Pure/Isar/runtime.ML Mon Aug 18 14:19:23 2014 +0200
@@ -16,6 +16,7 @@
val exn_messages: exn -> (serial * string) list
val exn_message: exn -> string
val exn_error_message: exn -> unit
+ val exn_system_message: exn -> unit
val exn_trace: (unit -> 'a) -> 'a
val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
@@ -135,6 +136,7 @@
| msgs => cat_lines (map snd msgs));
val exn_error_message = Output.error_message o exn_message;
+val exn_system_message = Output.system_message o exn_message;
fun exn_trace e = print_exception_trace exn_message e;
--- a/src/Pure/PIDE/document.scala Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Pure/PIDE/document.scala Mon Aug 18 14:19:23 2014 +0200
@@ -499,7 +499,9 @@
/*commands with markup produced by other commands (imm_succs)*/
val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
/*explicit (linear) history*/
- val history: History = History.init)
+ val history: History = History.init,
+ /*intermediate state between remove_versions/removed_versions*/
+ val removing_versions: Boolean = false)
{
private def fail[A]: A = throw new State.Fail(this)
@@ -620,13 +622,14 @@
copy(history = history + change)
}
- def prune_history(retain: Int = 0): (List[Version], State) =
+ def remove_versions(retain: Int = 0): (List[Version], State) =
{
history.prune(is_stable, retain) match {
case Some((dropped, history1)) =>
- val dropped_versions = dropped.map(change => change.version.get_finished)
- val state1 = copy(history = history1)
- (dropped_versions, state1)
+ val old_versions = dropped.map(change => change.version.get_finished)
+ val removing = !old_versions.isEmpty
+ val state1 = copy(history = history1, removing_versions = removing)
+ (old_versions, state1)
case None => fail
}
}
@@ -661,7 +664,8 @@
commands = commands1,
execs = execs1,
commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
- assignments = assignments1)
+ assignments = assignments1,
+ removing_versions = false)
}
private def command_states_self(version: Version, command: Command)
--- a/src/Pure/PIDE/markup.ML Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Mon Aug 18 14:19:23 2014 +0200
@@ -156,6 +156,7 @@
val tracingN: string
val warningN: string
val errorN: string
+ val systemN: string
val protocolN: string
val legacyN: string val legacy: T
val promptN: string val prompt: T
@@ -527,6 +528,7 @@
val tracingN = "tracing";
val warningN = "warning";
val errorN = "error";
+val systemN = "system";
val protocolN = "protocol";
val (legacyN, legacy) = markup_elem "legacy";
--- a/src/Pure/PIDE/session.scala Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Pure/PIDE/session.scala Mon Aug 18 14:19:23 2014 +0200
@@ -52,6 +52,8 @@
doc_edits: List[Document.Edit_Command],
version: Document.Version)
+ case object Change_Flush
+
/* events */
@@ -320,11 +322,10 @@
def store(change: Session.Change): Unit = synchronized { postponed ::= change }
- def flush(): Unit = synchronized {
- val state = global_state.value
+ def flush(state: Document.State): List[Session.Change] = synchronized {
val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
postponed = unassigned
- assigned.reverseIterator.foreach(change => manager.send(change))
+ assigned.reverse
}
}
@@ -448,9 +449,9 @@
try {
val cmds = global_state.change_result(_.assign(id, update))
change_buffer.invoke(true, cmds)
+ manager.send(Session.Change_Flush)
}
catch { case _: Document.State.Fail => bad_output() }
- postponed_changes.flush()
case _ => bad_output()
}
delay_prune.invoke()
@@ -460,6 +461,7 @@
case Protocol.Removed(removed) =>
try {
global_state.change(_.removed_versions(removed))
+ manager.send(Session.Change_Flush)
}
catch { case _: Document.State.Fail => bad_output() }
case _ => bad_output()
@@ -532,7 +534,7 @@
case Prune_History =>
if (prover.defined) {
- val old_versions = global_state.change_result(_.prune_history(prune_size))
+ val old_versions = global_state.change_result(_.remove_versions(prune_size))
if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
}
@@ -557,10 +559,16 @@
prover.get.protocol_command(name, args:_*)
case change: Session.Change if prover.defined =>
- if (global_state.value.is_assigned(change.previous))
+ val state = global_state.value
+ if (!state.removing_versions && state.is_assigned(change.previous))
handle_change(change)
else postponed_changes.store(change)
+ case Session.Change_Flush if prover.defined =>
+ val state = global_state.value
+ if (!state.removing_versions)
+ postponed_changes.flush(state).foreach(handle_change(_))
+
case bad =>
if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
}
--- a/src/Pure/System/isabelle_process.ML Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Aug 18 14:19:23 2014 +0200
@@ -124,6 +124,7 @@
Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
Output.error_message_fn :=
(fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
+ Output.system_message_fn := message Markup.systemN [];
Output.protocol_message_fn := message Markup.protocolN;
Output.urgent_message_fn := ! Output.writeln_fn;
Output.prompt_fn := ignore;
@@ -140,7 +141,8 @@
fun recover crash =
(Synchronized.change crashes (cons crash);
- warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
+ Output.physical_stderr
+ "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
fun read_chunk channel len =
let
@@ -170,10 +172,10 @@
fun loop channel =
let val continue =
(case read_command channel of
- [] => (Output.error_message "Isabelle process: no input"; true)
+ [] => (Output.system_message "Isabelle process: no input"; true)
| name :: args => (task_context (fn () => run_command name args); true))
handle Runtime.TERMINATE => false
- | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
+ | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
in
if continue then loop channel
else (Future.shutdown (); Execution.reset (); ())
--- a/src/Tools/jEdit/src/plugin.scala Mon Aug 18 14:09:21 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 18 14:19:23 2014 +0200
@@ -392,6 +392,7 @@
PIDE.session = new Session(resources) {
override def output_delay = PIDE.options.seconds("editor_output_delay")
override def prune_delay = PIDE.options.seconds("editor_prune_delay")
+ override def syslog_limit = PIDE.options.int("editor_syslog_limit")
override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}