--- a/.hgtags Wed May 22 22:18:45 2019 +0200
+++ b/.hgtags Mon May 27 16:47:17 2019 +0200
@@ -38,3 +38,4 @@
6f2ab7f150f6bb27d9e59229035324ce1f94e4ac Isabelle2019-RC0
9c60fcfdf495375cf1c886d7eb75583f63707950 Isabelle2019-RC1
805250bb7363dbfcb072ed34bbfb522106bdd21a Isabelle2019-RC2
+85de4fdec61b4c19b5491e61b637b66ae247ef97 Isabelle2019-RC3
--- a/ANNOUNCE Wed May 22 22:18:45 2019 +0200
+++ b/ANNOUNCE Mon May 27 16:47:17 2019 +0200
@@ -1,4 +1,4 @@
-Subject: Announcing Isabelle2018
+Subject: Announcing Isabelle2019
To: isabelle-users@cl.cam.ac.uk
Isabelle2019 is now available.
--- a/Admin/Windows/Installer/sfx.txt Wed May 22 22:18:45 2019 +0200
+++ b/Admin/Windows/Installer/sfx.txt Mon May 27 16:47:17 2019 +0200
@@ -1,6 +1,6 @@
;!@Install@!UTF-8!
GUIFlags="64"
-InstallPath="%%S"
+InstallPath="%UserDesktop%"
BeginPrompt="Unpack {ISABELLE_NAME}?"
ExtractPathText="Target directory"
ExtractTitle="Unpacking {ISABELLE_NAME} ..."
--- a/Admin/components/bundled-windows Wed May 22 22:18:45 2019 +0200
+++ b/Admin/components/bundled-windows Mon May 27 16:47:17 2019 +0200
@@ -1,3 +1,3 @@
#additional components to be bundled for release
-cygwin-20190322
+cygwin-20190524
windows_app-20181006
--- a/Admin/components/components.sha1 Wed May 22 22:18:45 2019 +0200
+++ b/Admin/components/components.sha1 Mon May 27 16:47:17 2019 +0200
@@ -10,6 +10,7 @@
bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz
81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz
97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz
+48b01bd9436e243ffcb7297f08b498d0c0875ed9 bash_process-1.2.3.tar.gz
9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz
a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz
4085dd6060a32d7e0d2e3f874c463a9964fd409b bib2xhtml-20190409.tar.gz
@@ -21,6 +22,7 @@
541eac340464c5d34b70bb163ae277cc8829c40f cvc4-1.5-2.tar.gz
1a44895d2a440091a15cc92d7f77a06a2e432507 cvc4-1.5-3.tar.gz
c0d8d5929b00e113752d8bf5d11241cd3bccafce cvc4-1.5-4.tar.gz
+ffb0d4739c10eb098eb092baef13eccf94a79bad cvc4-1.5-5.tar.gz
3682476dc5e915cf260764fa5b86f1ebdab57507 cvc4-1.5.tar.gz
a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz
4d9658fd2688ae8ac78da8fdfcbf85960f871b71 cvc4-1.5pre-2.tar.gz
@@ -50,6 +52,7 @@
5a3919e665947b820fd7f57787280c7512be3782 cygwin-20180604.tar.gz
2aa049170e8088de59bd70eed8220f552093932d cygwin-20190320.tar.gz
fb898e263fcf6f847d97f564fe49ea0760bb453f cygwin-20190322.tar.gz
+cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1 cygwin-20190524.tar.gz
0fe549949a025d65d52d6deca30554de8fca3b6e e-1.5.tar.gz
2e293256a134eb8e5b1a283361b15eb812fbfbf1 e-1.6-1.tar.gz
e1919e72416cbd7ac8de5455caba8901acc7b44d e-1.6-2.tar.gz
@@ -300,5 +303,6 @@
06b30757ff23aefbc30479785c212685ffd39f4d z3-4.3.2pre.tar.gz
93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8 z3-4.4.0pre-1.tar.gz
b1bc411c2083fc01577070b56b94514676f53854 z3-4.4.0pre-2.tar.gz
+4c366ab255d2e9343fb635d44d4d55ddd24c76d0 z3-4.4.0pre-3.tar.gz
517ba7b94c1985416c5b411c8ae84456367eb231 z3-4.4.0pre.tar.gz
aa20745f0b03e606b1a4149598e0c7572b63c657 z3-4.8.3.tar.gz
--- a/Admin/components/main Wed May 22 22:18:45 2019 +0200
+++ b/Admin/components/main Mon May 27 16:47:17 2019 +0200
@@ -1,8 +1,8 @@
#main components for everyday use, without big impact on overall build time
-bash_process-1.2.2
+bash_process-1.2.3
bib2xhtml-20190409
csdp-6.x
-cvc4-1.5-4
+cvc4-1.5-5
e-2.0-2
isabelle_fonts-20190409
jdk-11.0.3+7
@@ -22,4 +22,4 @@
stack-1.9.3
vampire-4.2.2
xz-java-1.8
-z3-4.4.0pre-2
+z3-4.4.0pre-3
--- a/NEWS Wed May 22 22:18:45 2019 +0200
+++ b/NEWS Mon May 27 16:47:17 2019 +0200
@@ -129,7 +129,7 @@
presentation context or to emit markup to the PIDE document. Some
predefined markers are taken from the Dublin Core Metadata Initiative,
e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
-can retrieved from the document database.
+can be retrieved from the document database.
* Old-style command tags %name are re-interpreted as markers with
proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
--- a/lib/Tools/update_op Wed May 22 22:18:45 2019 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Tobias Nipkow, TU Muenchen
-#
-# DESCRIPTION: update "op _" syntax
-
-## diagnostics
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
- echo
- echo " Options are:"
- echo " -m ignore .ML files"
- echo
- echo " Update the old \"op _\" syntax in theory and ML files."
- echo
- exit 1
-}
-
-
-IGNORE_ML=""
-
-while getopts "m" OPT
-do
- case "$OPT" in
- m)
- IGNORE_ML="true"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-DIR="."
-if [ -n "$1" ]; then
- DIR="$1"
-fi
-
-read -r -d '' THY_SCRIPT <<'EOF'
-# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
-s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
-# op *XY -> ( *XY)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
-# op *X -> ( *X)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
-# op *R -> ( *R)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
-# op *\<cdot> -> ( *\<cdot>)
-s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
-# op ** -> ( ** )
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
-# op * -> ( * )
-s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
-# (op +) -> (+)
-s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
-# (op + -> ((+)
-s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
-# op + -> (+)
-s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
-s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
-# op+ -> (+)
-s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
-s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
-s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
-EOF
-
-read -r -d '' ML_SCRIPT <<'EOF'
-# op * -> ( * )
-s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
-s/"op[ ]*\*/"( \* )/g
-# (op +) -> (+)
-s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
-s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
-# (op + -> ((+)
-s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
-# op + -> (+)
-s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
-s/"op [ ]*\([^ )("]*\)/"(\1)/g
-# op+ -> (+)
-s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
-s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
-# is there \<...\> on the line (indicating Isabelle source):
-s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
-s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
-s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
-s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
-EOF
-
-find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
-
-[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
-
--- a/src/Doc/JEdit/JEdit.thy Wed May 22 22:18:45 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy Mon May 27 16:47:17 2019 +0200
@@ -2152,7 +2152,7 @@
(by Oracle) on low-quality displays.
\<^bold>\<open>Workaround:\<close> Find an old copy of Java 8 from Oracle (which has
- ``end-of-live'' status since Jan-2019) and refer to its main directory via
+ ``end-of-life'' status since Jan-2019) and refer to its main directory via
@{setting "ISABELLE_JDK_HOME"}\<^verbatim>\<open>="..."\<close> in
\<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. Also add
\<^verbatim>\<open>isabelle_fonts_hinted=false\<close> to
--- a/src/HOL/Tools/SMT/smt_solver.ML Wed May 22 22:18:45 2019 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Mon May 27 16:47:17 2019 +0200
@@ -49,9 +49,9 @@
local
fun make_command command options problem_path proof_path =
- "(exec 2>&1;" :: map Bash.string (command () @ options) @
- [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
- |> space_implode " "
+ Bash.strings (command () @ options) ^ " " ^
+ Bash.string (File.platform_path problem_path) ^
+ " > " ^ File.bash_path proof_path ^ " 2>&1"
fun with_trace ctxt msg f x =
let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
--- a/src/HOL/Types_To_Sets/unoverload_type.ML Wed May 22 22:18:45 2019 +0200
+++ b/src/HOL/Types_To_Sets/unoverload_type.ML Mon May 27 16:47:17 2019 +0200
@@ -16,7 +16,7 @@
fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
fun params_of_super_classes thy class =
- Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
+ class::Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
--- a/src/Pure/General/file.ML Wed May 22 22:18:45 2019 +0200
+++ b/src/Pure/General/file.ML Mon May 27 16:47:17 2019 +0200
@@ -50,6 +50,7 @@
val bash_path = Bash_Syntax.string o standard_path;
val bash_paths = Bash_Syntax.strings o map standard_path;
+
(* full_path *)
fun full_path dir path =
--- a/src/Pure/PIDE/document.ML Wed May 22 22:18:45 2019 +0200
+++ b/src/Pure/PIDE/document.ML Mon May 27 16:47:17 2019 +0200
@@ -25,7 +25,7 @@
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
- Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
+ string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
val state: unit -> state
val change_state: (state -> state) -> unit
end;
@@ -294,11 +294,14 @@
(String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
nodes);
+fun is_suppressed_node (nodes: node String_Graph.T) (name, node) =
+ String_Graph.is_maximal nodes name andalso is_empty_node node;
+
fun put_node (name, node) (Version nodes) =
let
val nodes1 = update_node name (K node) nodes;
val nodes2 =
- if String_Graph.is_maximal nodes1 name andalso is_empty_node node
+ if is_suppressed_node nodes1 (name, node)
then String_Graph.del_node name nodes1
else nodes1;
in Version nodes2 end;
@@ -809,7 +812,8 @@
forall (fn (name, (_, node)) => check_theory true name node) imports;
val (print_execs, common, (still_visible, initial)) =
- if imports_result_changed then (assign_update_empty, NONE, (true, true))
+ if imports_result_changed
+ then (assign_update_empty, NONE, (true, true))
else last_common keywords state node_required node0 node;
val common_command_exec =
@@ -865,7 +869,7 @@
val state' = state
|> define_version new_version_id new_version assigned_nodes;
- in (removed, assign_result, state') end);
+ in (Symtab.keys edited, removed, assign_result, state') end);
end;
--- a/src/Pure/PIDE/document.scala Wed May 22 22:18:45 2019 +0200
+++ b/src/Pure/PIDE/document.scala Mon May 27 16:47:17 2019 +0200
@@ -651,7 +651,7 @@
}
val init: State =
- State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
+ State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
}
final case class State private(
@@ -768,10 +768,15 @@
st <- command_states(version, command).iterator
} yield st.exports)
- def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
+ def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
+ : ((List[Node.Name], List[Command]), State) =
{
val version = the_version(id)
+ val edited_set = edited.toSet
+ val edited_nodes =
+ (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
+
def upd(exec_id: Document_ID.Exec, st: Command.State)
: Option[(Document_ID.Exec, Command.State)] =
if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
@@ -794,7 +799,7 @@
val new_assignment = the_assignment(version).assign(update)
val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
- (changed_commands, new_state)
+ ((edited_nodes, changed_commands), new_state)
}
def is_assigned(version: Version): Boolean =
--- a/src/Pure/PIDE/protocol.ML Wed May 22 22:18:45 2019 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon May 27 16:47:17 2019 +0200
@@ -106,7 +106,7 @@
val _ = Execution.discontinue ();
- val (removed, assign_update, state') =
+ val (edited, removed, assign_update, state') =
Document.update old_id new_id edits consolidate state;
val _ =
(singleton o Future.forks)
@@ -117,12 +117,12 @@
val _ =
Output.protocol_message Markup.assign_update
- ((new_id, assign_update) |>
+ ((new_id, edited, assign_update) |>
let
open XML.Encode;
fun encode_upd (a, bs) =
string (space_implode "," (map Value.print_int (a :: bs)));
- in pair int (list encode_upd) end
+ in triple int (list string) (list encode_upd) end
|> YXML.chunks_of_body);
in Document.start_execution state' end)));
--- a/src/Pure/PIDE/protocol.scala Wed May 22 22:18:45 2019 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon May 27 16:47:17 2019 +0200
@@ -13,7 +13,9 @@
object Assign_Update
{
- def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
+ def unapply(text: String)
+ : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
+ {
try {
import XML.Decode._
def decode_upd(body: XML.Body): (Long, List[Long]) =
@@ -21,12 +23,13 @@
case a :: bs => (a, bs)
case _ => throw new XML.XML_Body(body)
}
- Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
+ Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
}
catch {
case ERROR(_) => None
case _: XML.Error => None
}
+ }
}
object Removed
--- a/src/Pure/PIDE/session.scala Wed May 22 22:18:45 2019 +0200
+++ b/src/Pure/PIDE/session.scala Mon May 27 16:47:17 2019 +0200
@@ -269,15 +269,19 @@
}
private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
- def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
- assignment |= assign
- for (command <- cmds) {
- nodes += command.node_name
- command.blobs_names.foreach(nodes += _)
- commands += command
+ def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
+ synchronized {
+ assignment |= assign
+ for (node <- edited_nodes) {
+ nodes += node
+ }
+ for (command <- cmds) {
+ nodes += command.node_name
+ command.blobs_names.foreach(nodes += _)
+ commands += command
+ }
+ delay_flush.invoke()
}
- delay_flush.invoke()
- }
def shutdown()
{
@@ -457,7 +461,7 @@
{
try {
val st = global_state.change_result(f)
- change_buffer.invoke(false, List(st.command))
+ change_buffer.invoke(false, Nil, List(st.command))
}
catch { case _: Document.State.Fail => bad_output() }
}
@@ -485,10 +489,11 @@
case Markup.Assign_Update =>
msg.text match {
- case Protocol.Assign_Update(id, update) =>
+ case Protocol.Assign_Update(id, edited, update) =>
try {
- val cmds = global_state.change_result(_.assign(id, update))
- change_buffer.invoke(true, cmds)
+ val (edited_nodes, cmds) =
+ global_state.change_result(_.assign(id, edited, update))
+ change_buffer.invoke(true, edited_nodes, cmds)
manager.send(Session.Change_Flush)
}
catch { case _: Document.State.Fail => bad_output() }
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed May 22 22:18:45 2019 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon May 27 16:47:17 2019 +0200
@@ -48,7 +48,7 @@
val state1 =
state0.continue_history(Future.value(version0), edits, Future.value(version1))
.define_version(version1, state0.the_assignment(version0))
- .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
+ .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
(command.source, state1)
}
--- a/src/Tools/jEdit/src/query_dockable.scala Wed May 22 22:18:45 2019 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Mon May 27 16:47:17 2019 +0200
@@ -92,7 +92,7 @@
private val query_label = new Label("Find:") {
tooltip =
GUI.tooltip_lines(
- "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
+ "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
}
val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)