merged
authorwenzelm
Mon Aug 18 14:19:23 2014 +0200 (2014-08-18)
changeset 57980381b3c4fc75a
parent 57971 07e81758788d
parent 57979 fc136831d6ca
child 57981 81baacfd56e8
merged
     1.1 --- a/.hgtags	Mon Aug 18 14:09:21 2014 +0200
     1.2 +++ b/.hgtags	Mon Aug 18 14:19:23 2014 +0200
     1.3 @@ -32,3 +32,4 @@
     1.4  c0fd03d13d28954f6b7018f273b6edb17fcdeaf7 Isabelle2014-RC1
     1.5  ee908fccabc220a5f2e5af533d13ebceeb0e09ff Isabelle2014-RC2
     1.6  91e188508bc9df5de2737325c390836603a3e409 Isabelle2014-RC3
     1.7 +113b43b84412416c67dc5e46f0d79473c837fbda Isabelle2014-RC4
     2.1 --- a/Admin/components/bundled-windows	Mon Aug 18 14:09:21 2014 +0200
     2.2 +++ b/Admin/components/bundled-windows	Mon Aug 18 14:19:23 2014 +0200
     2.3 @@ -1,3 +1,3 @@
     2.4  #additional components to be bundled for release
     2.5 -cygwin-20140725
     2.6 +cygwin-20140813
     2.7  windows_app-20131201
     3.1 --- a/Admin/components/components.sha1	Mon Aug 18 14:09:21 2014 +0200
     3.2 +++ b/Admin/components/components.sha1	Mon Aug 18 14:19:23 2014 +0200
     3.3 @@ -9,6 +9,7 @@
     3.4  acbc4bf161ad21e96ecfe506266ccdbd288f8a6f  cygwin-20140530.tar.gz
     3.5  3dc680d9eb85276e8c3e9f6057dad0efe2d5aa41  cygwin-20140626.tar.gz
     3.6  8e562dfe57a2f894f9461f4addedb88afa108152  cygwin-20140725.tar.gz
     3.7 +238d8e30e8e22495b7ea3f5ec36e852e97fe8bbf  cygwin-20140813.tar.gz
     3.8  0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
     3.9  2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
    3.10  e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
    3.11 @@ -29,6 +30,7 @@
    3.12  dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c  jdk-7u40.tar.gz
    3.13  71b629b2ce83dbb69967c4785530afce1bec3809  jdk-7u60.tar.gz
    3.14  e119f4cbfa2a39a53b9578d165d0dc44b59527b7  jdk-7u65.tar.gz
    3.15 +d6d1c42989433839fe64f34eb77298ef6627aed4  jdk-7u67.tar.gz
    3.16  ec740ee9ffd43551ddf1e5b91641405116af6291  jdk-7u6.tar.gz
    3.17  7d5b152ac70f720bb9e783fa45ecadcf95069584  jdk-7u9.tar.gz
    3.18  5442f1015a0657259be0590b04572cd933431df7  jdk-8u11.tar.gz
     4.1 --- a/Admin/components/main	Mon Aug 18 14:09:21 2014 +0200
     4.2 +++ b/Admin/components/main	Mon Aug 18 14:19:23 2014 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4  e-1.8
     4.5  exec_process-1.0.3
     4.6  Haskabelle-2014
     4.7 -jdk-7u65
     4.8 +jdk-7u67
     4.9  jedit_build-20140722
    4.10  jfreechart-1.0.14-1
    4.11  jortho-1.0-2
     5.1 --- a/Admin/java/build	Mon Aug 18 14:09:21 2014 +0200
     5.2 +++ b/Admin/java/build	Mon Aug 18 14:19:23 2014 +0200
     5.3 @@ -11,8 +11,8 @@
     5.4  
     5.5  ## parameters
     5.6  
     5.7 -VERSION="7u65"
     5.8 -FULL_VERSION="1.7.0_65"
     5.9 +VERSION="7u67"
    5.10 +FULL_VERSION="1.7.0_67"
    5.11  
    5.12  ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
    5.13  ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
     6.1 --- a/etc/options	Mon Aug 18 14:09:21 2014 +0200
     6.2 +++ b/etc/options	Mon Aug 18 14:19:23 2014 +0200
     6.3 @@ -138,6 +138,9 @@
     6.4  option editor_execution_delay : real = 0.02
     6.5    -- "delay for start of execution process after document update (seconds)"
     6.6  
     6.7 +option editor_syslog_limit : int = 100
     6.8 +  -- "maximum amount of buffered syslog messages"
     6.9 +
    6.10  
    6.11  section "Miscellaneous Tools"
    6.12  
     7.1 --- a/src/Doc/Isar_Ref/Proof.thy	Mon Aug 18 14:09:21 2014 +0200
     7.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Mon Aug 18 14:19:23 2014 +0200
     7.3 @@ -520,10 +520,10 @@
     7.4    \secref{sec:term-abbrev}.
     7.5  
     7.6    The optional case names of @{element_ref "obtains"} have a twofold
     7.7 -  meaning: (1) during the of this claim they refer to the the local
     7.8 -  context introductions, (2) the resulting rule is annotated
     7.9 -  accordingly to support symbolic case splits when used with the
    7.10 -  @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
    7.11 +  meaning: (1) in the proof of this claim they refer to the local context
    7.12 +  introductions, (2) in the resulting rule they become annotations for
    7.13 +  symbolic case splits, e.g.\ for the @{method_ref cases} method
    7.14 +  (\secref{sec:cases-induct}).
    7.15  *}
    7.16  
    7.17  
     8.1 --- a/src/Pure/General/output.ML	Mon Aug 18 14:09:21 2014 +0200
     8.2 +++ b/src/Pure/General/output.ML	Mon Aug 18 14:19:23 2014 +0200
     8.3 @@ -29,6 +29,7 @@
     8.4    val urgent_message: string -> unit
     8.5    val error_message': serial * string -> unit
     8.6    val error_message: string -> unit
     8.7 +  val system_message: string -> unit
     8.8    val prompt: string -> unit
     8.9    val status: string -> unit
    8.10    val report: string list -> unit
    8.11 @@ -45,6 +46,7 @@
    8.12    val tracing_fn: (output list -> unit) Unsynchronized.ref
    8.13    val warning_fn: (output list -> unit) Unsynchronized.ref
    8.14    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    8.15 +  val system_message_fn: (output list -> unit) Unsynchronized.ref
    8.16    val prompt_fn: (output -> unit) Unsynchronized.ref
    8.17    val status_fn: (output list -> unit) Unsynchronized.ref
    8.18    val report_fn: (output list -> unit) Unsynchronized.ref
    8.19 @@ -101,6 +103,7 @@
    8.20  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    8.21  val error_message_fn =
    8.22    Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    8.23 +val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    8.24  val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
    8.25  val status_fn = Unsynchronized.ref (fn _: output list => ());
    8.26  val report_fn = Unsynchronized.ref (fn _: output list => ());
    8.27 @@ -115,6 +118,7 @@
    8.28  fun warning s = ! warning_fn [output s];
    8.29  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    8.30  fun error_message s = error_message' (serial (), s);
    8.31 +fun system_message s = ! system_message_fn [output s];
    8.32  fun prompt s = ! prompt_fn (output s);
    8.33  fun status s = ! status_fn [output s];
    8.34  fun report ss = ! report_fn (map output ss);
     9.1 --- a/src/Pure/Isar/runtime.ML	Mon Aug 18 14:09:21 2014 +0200
     9.2 +++ b/src/Pure/Isar/runtime.ML	Mon Aug 18 14:19:23 2014 +0200
     9.3 @@ -16,6 +16,7 @@
     9.4    val exn_messages: exn -> (serial * string) list
     9.5    val exn_message: exn -> string
     9.6    val exn_error_message: exn -> unit
     9.7 +  val exn_system_message: exn -> unit
     9.8    val exn_trace: (unit -> 'a) -> 'a
     9.9    val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    9.10    val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    9.11 @@ -135,6 +136,7 @@
    9.12    | msgs => cat_lines (map snd msgs));
    9.13  
    9.14  val exn_error_message = Output.error_message o exn_message;
    9.15 +val exn_system_message = Output.system_message o exn_message;
    9.16  fun exn_trace e = print_exception_trace exn_message e;
    9.17  
    9.18  
    10.1 --- a/src/Pure/PIDE/document.scala	Mon Aug 18 14:09:21 2014 +0200
    10.2 +++ b/src/Pure/PIDE/document.scala	Mon Aug 18 14:19:23 2014 +0200
    10.3 @@ -499,7 +499,9 @@
    10.4      /*commands with markup produced by other commands (imm_succs)*/
    10.5      val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
    10.6      /*explicit (linear) history*/
    10.7 -    val history: History = History.init)
    10.8 +    val history: History = History.init,
    10.9 +    /*intermediate state between remove_versions/removed_versions*/
   10.10 +    val removing_versions: Boolean = false)
   10.11    {
   10.12      private def fail[A]: A = throw new State.Fail(this)
   10.13  
   10.14 @@ -620,13 +622,14 @@
   10.15        copy(history = history + change)
   10.16      }
   10.17  
   10.18 -    def prune_history(retain: Int = 0): (List[Version], State) =
   10.19 +    def remove_versions(retain: Int = 0): (List[Version], State) =
   10.20      {
   10.21        history.prune(is_stable, retain) match {
   10.22          case Some((dropped, history1)) =>
   10.23 -          val dropped_versions = dropped.map(change => change.version.get_finished)
   10.24 -          val state1 = copy(history = history1)
   10.25 -          (dropped_versions, state1)
   10.26 +          val old_versions = dropped.map(change => change.version.get_finished)
   10.27 +          val removing = !old_versions.isEmpty
   10.28 +          val state1 = copy(history = history1, removing_versions = removing)
   10.29 +          (old_versions, state1)
   10.30          case None => fail
   10.31        }
   10.32      }
   10.33 @@ -661,7 +664,8 @@
   10.34          commands = commands1,
   10.35          execs = execs1,
   10.36          commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
   10.37 -        assignments = assignments1)
   10.38 +        assignments = assignments1,
   10.39 +        removing_versions = false)
   10.40      }
   10.41  
   10.42      private def command_states_self(version: Version, command: Command)
    11.1 --- a/src/Pure/PIDE/markup.ML	Mon Aug 18 14:09:21 2014 +0200
    11.2 +++ b/src/Pure/PIDE/markup.ML	Mon Aug 18 14:19:23 2014 +0200
    11.3 @@ -156,6 +156,7 @@
    11.4    val tracingN: string
    11.5    val warningN: string
    11.6    val errorN: string
    11.7 +  val systemN: string
    11.8    val protocolN: string
    11.9    val legacyN: string val legacy: T
   11.10    val promptN: string val prompt: T
   11.11 @@ -527,6 +528,7 @@
   11.12  val tracingN = "tracing";
   11.13  val warningN = "warning";
   11.14  val errorN = "error";
   11.15 +val systemN = "system";
   11.16  val protocolN = "protocol";
   11.17  
   11.18  val (legacyN, legacy) = markup_elem "legacy";
    12.1 --- a/src/Pure/PIDE/session.scala	Mon Aug 18 14:09:21 2014 +0200
    12.2 +++ b/src/Pure/PIDE/session.scala	Mon Aug 18 14:19:23 2014 +0200
    12.3 @@ -52,6 +52,8 @@
    12.4      doc_edits: List[Document.Edit_Command],
    12.5      version: Document.Version)
    12.6  
    12.7 +  case object Change_Flush
    12.8 +
    12.9  
   12.10    /* events */
   12.11  
   12.12 @@ -320,11 +322,10 @@
   12.13  
   12.14      def store(change: Session.Change): Unit = synchronized { postponed ::= change }
   12.15  
   12.16 -    def flush(): Unit = synchronized {
   12.17 -      val state = global_state.value
   12.18 +    def flush(state: Document.State): List[Session.Change] = synchronized {
   12.19        val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous))
   12.20        postponed = unassigned
   12.21 -      assigned.reverseIterator.foreach(change => manager.send(change))
   12.22 +      assigned.reverse
   12.23      }
   12.24    }
   12.25  
   12.26 @@ -448,9 +449,9 @@
   12.27                      try {
   12.28                        val cmds = global_state.change_result(_.assign(id, update))
   12.29                        change_buffer.invoke(true, cmds)
   12.30 +                      manager.send(Session.Change_Flush)
   12.31                      }
   12.32                      catch { case _: Document.State.Fail => bad_output() }
   12.33 -                    postponed_changes.flush()
   12.34                    case _ => bad_output()
   12.35                  }
   12.36                  delay_prune.invoke()
   12.37 @@ -460,6 +461,7 @@
   12.38                    case Protocol.Removed(removed) =>
   12.39                      try {
   12.40                        global_state.change(_.removed_versions(removed))
   12.41 +                      manager.send(Session.Change_Flush)
   12.42                      }
   12.43                      catch { case _: Document.State.Fail => bad_output() }
   12.44                    case _ => bad_output()
   12.45 @@ -532,7 +534,7 @@
   12.46  
   12.47            case Prune_History =>
   12.48              if (prover.defined) {
   12.49 -              val old_versions = global_state.change_result(_.prune_history(prune_size))
   12.50 +              val old_versions = global_state.change_result(_.remove_versions(prune_size))
   12.51                if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
   12.52              }
   12.53  
   12.54 @@ -557,10 +559,16 @@
   12.55              prover.get.protocol_command(name, args:_*)
   12.56  
   12.57            case change: Session.Change if prover.defined =>
   12.58 -            if (global_state.value.is_assigned(change.previous))
   12.59 +            val state = global_state.value
   12.60 +            if (!state.removing_versions && state.is_assigned(change.previous))
   12.61                handle_change(change)
   12.62              else postponed_changes.store(change)
   12.63  
   12.64 +          case Session.Change_Flush if prover.defined =>
   12.65 +            val state = global_state.value
   12.66 +            if (!state.removing_versions)
   12.67 +              postponed_changes.flush(state).foreach(handle_change(_))
   12.68 +
   12.69            case bad =>
   12.70              if (verbose) Output.warning("Ignoring bad message: " + bad.toString)
   12.71          }
    13.1 --- a/src/Pure/System/isabelle_process.ML	Mon Aug 18 14:09:21 2014 +0200
    13.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Aug 18 14:19:23 2014 +0200
    13.3 @@ -124,6 +124,7 @@
    13.4      Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    13.5      Output.error_message_fn :=
    13.6        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    13.7 +    Output.system_message_fn := message Markup.systemN [];
    13.8      Output.protocol_message_fn := message Markup.protocolN;
    13.9      Output.urgent_message_fn := ! Output.writeln_fn;
   13.10      Output.prompt_fn := ignore;
   13.11 @@ -140,7 +141,8 @@
   13.12  
   13.13  fun recover crash =
   13.14    (Synchronized.change crashes (cons crash);
   13.15 -    warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
   13.16 +    Output.physical_stderr
   13.17 +      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
   13.18  
   13.19  fun read_chunk channel len =
   13.20    let
   13.21 @@ -170,10 +172,10 @@
   13.22  fun loop channel =
   13.23    let val continue =
   13.24      (case read_command channel of
   13.25 -      [] => (Output.error_message "Isabelle process: no input"; true)
   13.26 +      [] => (Output.system_message "Isabelle process: no input"; true)
   13.27      | name :: args => (task_context (fn () => run_command name args); true))
   13.28      handle Runtime.TERMINATE => false
   13.29 -      | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
   13.30 +      | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   13.31    in
   13.32      if continue then loop channel
   13.33      else (Future.shutdown (); Execution.reset (); ())
    14.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 18 14:09:21 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 18 14:19:23 2014 +0200
    14.3 @@ -392,6 +392,7 @@
    14.4        PIDE.session = new Session(resources) {
    14.5          override def output_delay = PIDE.options.seconds("editor_output_delay")
    14.6          override def prune_delay = PIDE.options.seconds("editor_prune_delay")
    14.7 +        override def syslog_limit = PIDE.options.int("editor_syslog_limit")
    14.8          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
    14.9        }
   14.10