# HG changeset patch # User wenzelm # Date 1408360744 -7200 # Node ID fc136831d6cad9c5df83d043c3591ec930e77801 # Parent 6fab7e95587d0911ae07ae542f71d6af6a399f7f# Parent 8f4a332500e41bb67efc3e141608829473606a72 merged; diff -r 6fab7e95587d -r fc136831d6ca .hgtags --- a/.hgtags Sun Aug 17 22:27:58 2014 +0200 +++ b/.hgtags Mon Aug 18 13:19:04 2014 +0200 @@ -32,3 +32,4 @@ c0fd03d13d28954f6b7018f273b6edb17fcdeaf7 Isabelle2014-RC1 ee908fccabc220a5f2e5af533d13ebceeb0e09ff Isabelle2014-RC2 91e188508bc9df5de2737325c390836603a3e409 Isabelle2014-RC3 +113b43b84412416c67dc5e46f0d79473c837fbda Isabelle2014-RC4 diff -r 6fab7e95587d -r fc136831d6ca Admin/components/bundled-windows --- a/Admin/components/bundled-windows Sun Aug 17 22:27:58 2014 +0200 +++ b/Admin/components/bundled-windows Mon Aug 18 13:19:04 2014 +0200 @@ -1,3 +1,3 @@ #additional components to be bundled for release -cygwin-20140725 +cygwin-20140813 windows_app-20131201 diff -r 6fab7e95587d -r fc136831d6ca Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sun Aug 17 22:27:58 2014 +0200 +++ b/Admin/components/components.sha1 Mon Aug 18 13:19:04 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 diff -r 6fab7e95587d -r fc136831d6ca Admin/components/main --- a/Admin/components/main Sun Aug 17 22:27:58 2014 +0200 +++ b/Admin/components/main Mon Aug 18 13:19:04 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 diff -r 6fab7e95587d -r fc136831d6ca Admin/java/build --- a/Admin/java/build Sun Aug 17 22:27:58 2014 +0200 +++ b/Admin/java/build Mon Aug 18 13:19:04 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" diff -r 6fab7e95587d -r fc136831d6ca etc/options --- a/etc/options Sun Aug 17 22:27:58 2014 +0200 +++ b/etc/options Mon Aug 18 13:19:04 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" diff -r 6fab7e95587d -r fc136831d6ca src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Doc/Isar_Ref/Proof.thy Mon Aug 18 13:19:04 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}). *} diff -r 6fab7e95587d -r fc136831d6ca src/Pure/General/output.ML --- a/src/Pure/General/output.ML Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Pure/General/output.ML Mon Aug 18 13:19:04 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); diff -r 6fab7e95587d -r fc136831d6ca src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Pure/Isar/runtime.ML Mon Aug 18 13:19:04 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; diff -r 6fab7e95587d -r fc136831d6ca src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Pure/PIDE/document.scala Mon Aug 18 13:19:04 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) diff -r 6fab7e95587d -r fc136831d6ca src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Pure/PIDE/markup.ML Mon Aug 18 13:19:04 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"; diff -r 6fab7e95587d -r fc136831d6ca src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Pure/PIDE/session.scala Mon Aug 18 13:19:04 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) } diff -r 6fab7e95587d -r fc136831d6ca src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Pure/System/isabelle_process.ML Mon Aug 18 13:19:04 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 (); ()) diff -r 6fab7e95587d -r fc136831d6ca src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Aug 17 22:27:58 2014 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 18 13:19:04 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") }