# HG changeset patch # User wenzelm # Date 1558968437 -7200 # Node ID 742f8e7037802b2f870e07e2d3660931fd43a84f # Parent ac24aaf84a3657b2e7d39a7300ce81c076735c80# Parent c7e9d3a0a681f73781febb6e8a825bfe724d4c1a merged diff -r ac24aaf84a36 -r 742f8e703780 .hgtags --- 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 diff -r ac24aaf84a36 -r 742f8e703780 ANNOUNCE --- 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. diff -r ac24aaf84a36 -r 742f8e703780 Admin/Windows/Installer/sfx.txt --- 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} ..." diff -r ac24aaf84a36 -r 742f8e703780 Admin/components/bundled-windows --- 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 diff -r ac24aaf84a36 -r 742f8e703780 Admin/components/components.sha1 --- 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 diff -r ac24aaf84a36 -r 742f8e703780 Admin/components/main --- 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 diff -r ac24aaf84a36 -r 742f8e703780 NEWS --- 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>\contributor arg\ or \<^marker>\license arg\ 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>\tag (proof) name\ and produce LaTeX environments as diff -r ac24aaf84a36 -r 742f8e703780 lib/Tools/update_op --- 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 *\ -> ( *\) -s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\\)/\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 [ ]*\([^ )("]*\)\\/\\<\1>\2\3(\4)\\/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" {} \; - diff -r ac24aaf84a36 -r 742f8e703780 src/Doc/JEdit/JEdit.thy --- 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>\Workaround:\ 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>\="..."\ in \<^path>\$ISABELLE_HOME_USER/etc/settings\. Also add \<^verbatim>\isabelle_fonts_hinted=false\ to diff -r ac24aaf84a36 -r 742f8e703780 src/HOL/Tools/SMT/smt_solver.ML --- 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) () diff -r ac24aaf84a36 -r 742f8e703780 src/HOL/Types_To_Sets/unoverload_type.ML --- 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 diff -r ac24aaf84a36 -r 742f8e703780 src/Pure/General/file.ML --- 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 = diff -r ac24aaf84a36 -r 742f8e703780 src/Pure/PIDE/document.ML --- 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; diff -r ac24aaf84a36 -r 742f8e703780 src/Pure/PIDE/document.scala --- 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 = diff -r ac24aaf84a36 -r 742f8e703780 src/Pure/PIDE/protocol.ML --- 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))); diff -r ac24aaf84a36 -r 742f8e703780 src/Pure/PIDE/protocol.scala --- 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 diff -r ac24aaf84a36 -r 742f8e703780 src/Pure/PIDE/session.scala --- 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() } diff -r ac24aaf84a36 -r 742f8e703780 src/Tools/jEdit/src/pretty_text_area.scala --- 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) } diff -r ac24aaf84a36 -r 742f8e703780 src/Tools/jEdit/src/query_dockable.scala --- 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 _)