merged
authorwenzelm
Mon May 27 16:47:17 2019 +0200 (8 weeks ago)
changeset 70294742f8e703780
parent 70277 ac24aaf84a36
parent 70293 c7e9d3a0a681
child 70295 39f5db308fe0
merged
NEWS
lib/Tools/update_op
     1.1 --- a/.hgtags	Wed May 22 22:18:45 2019 +0200
     1.2 +++ b/.hgtags	Mon May 27 16:47:17 2019 +0200
     1.3 @@ -38,3 +38,4 @@
     1.4  6f2ab7f150f6bb27d9e59229035324ce1f94e4ac Isabelle2019-RC0
     1.5  9c60fcfdf495375cf1c886d7eb75583f63707950 Isabelle2019-RC1
     1.6  805250bb7363dbfcb072ed34bbfb522106bdd21a Isabelle2019-RC2
     1.7 +85de4fdec61b4c19b5491e61b637b66ae247ef97 Isabelle2019-RC3
     2.1 --- a/ANNOUNCE	Wed May 22 22:18:45 2019 +0200
     2.2 +++ b/ANNOUNCE	Mon May 27 16:47:17 2019 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -Subject: Announcing Isabelle2018
     2.5 +Subject: Announcing Isabelle2019
     2.6  To: isabelle-users@cl.cam.ac.uk
     2.7  
     2.8  Isabelle2019 is now available.
     3.1 --- a/Admin/Windows/Installer/sfx.txt	Wed May 22 22:18:45 2019 +0200
     3.2 +++ b/Admin/Windows/Installer/sfx.txt	Mon May 27 16:47:17 2019 +0200
     3.3 @@ -1,6 +1,6 @@
     3.4  ;!@Install@!UTF-8!
     3.5  GUIFlags="64"
     3.6 -InstallPath="%%S"
     3.7 +InstallPath="%UserDesktop%"
     3.8  BeginPrompt="Unpack {ISABELLE_NAME}?"
     3.9  ExtractPathText="Target directory"
    3.10  ExtractTitle="Unpacking {ISABELLE_NAME} ..."
     4.1 --- a/Admin/components/bundled-windows	Wed May 22 22:18:45 2019 +0200
     4.2 +++ b/Admin/components/bundled-windows	Mon May 27 16:47:17 2019 +0200
     4.3 @@ -1,3 +1,3 @@
     4.4  #additional components to be bundled for release
     4.5 -cygwin-20190322
     4.6 +cygwin-20190524
     4.7  windows_app-20181006
     5.1 --- a/Admin/components/components.sha1	Wed May 22 22:18:45 2019 +0200
     5.2 +++ b/Admin/components/components.sha1	Mon May 27 16:47:17 2019 +0200
     5.3 @@ -10,6 +10,7 @@
     5.4  bb9ef498cd594b4289221b96146d529c899da209  bash_process-1.1.tar.gz
     5.5  81250148f8b89ac3587908fb20645081d7f53207  bash_process-1.2.1.tar.gz
     5.6  97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
     5.7 +48b01bd9436e243ffcb7297f08b498d0c0875ed9  bash_process-1.2.3.tar.gz
     5.8  9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
     5.9  a65ce644b6094d41e9f991ef851cf05eff5dd0a9  bib2xhtml-20171221.tar.gz
    5.10  4085dd6060a32d7e0d2e3f874c463a9964fd409b  bib2xhtml-20190409.tar.gz
    5.11 @@ -21,6 +22,7 @@
    5.12  541eac340464c5d34b70bb163ae277cc8829c40f  cvc4-1.5-2.tar.gz
    5.13  1a44895d2a440091a15cc92d7f77a06a2e432507  cvc4-1.5-3.tar.gz
    5.14  c0d8d5929b00e113752d8bf5d11241cd3bccafce  cvc4-1.5-4.tar.gz
    5.15 +ffb0d4739c10eb098eb092baef13eccf94a79bad  cvc4-1.5-5.tar.gz
    5.16  3682476dc5e915cf260764fa5b86f1ebdab57507  cvc4-1.5.tar.gz
    5.17  a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
    5.18  4d9658fd2688ae8ac78da8fdfcbf85960f871b71  cvc4-1.5pre-2.tar.gz
    5.19 @@ -50,6 +52,7 @@
    5.20  5a3919e665947b820fd7f57787280c7512be3782  cygwin-20180604.tar.gz
    5.21  2aa049170e8088de59bd70eed8220f552093932d  cygwin-20190320.tar.gz
    5.22  fb898e263fcf6f847d97f564fe49ea0760bb453f  cygwin-20190322.tar.gz
    5.23 +cd01fac0ab4fdb50a2bbb6416da3f15a4d540da1  cygwin-20190524.tar.gz
    5.24  0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
    5.25  2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
    5.26  e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
    5.27 @@ -300,5 +303,6 @@
    5.28  06b30757ff23aefbc30479785c212685ffd39f4d  z3-4.3.2pre.tar.gz
    5.29  93e7e4bddc6afcf87fe2b6656cfcb1b1acd0a4f8  z3-4.4.0pre-1.tar.gz
    5.30  b1bc411c2083fc01577070b56b94514676f53854  z3-4.4.0pre-2.tar.gz
    5.31 +4c366ab255d2e9343fb635d44d4d55ddd24c76d0  z3-4.4.0pre-3.tar.gz
    5.32  517ba7b94c1985416c5b411c8ae84456367eb231  z3-4.4.0pre.tar.gz
    5.33  aa20745f0b03e606b1a4149598e0c7572b63c657  z3-4.8.3.tar.gz
     6.1 --- a/Admin/components/main	Wed May 22 22:18:45 2019 +0200
     6.2 +++ b/Admin/components/main	Mon May 27 16:47:17 2019 +0200
     6.3 @@ -1,8 +1,8 @@
     6.4  #main components for everyday use, without big impact on overall build time
     6.5 -bash_process-1.2.2
     6.6 +bash_process-1.2.3
     6.7  bib2xhtml-20190409
     6.8  csdp-6.x
     6.9 -cvc4-1.5-4
    6.10 +cvc4-1.5-5
    6.11  e-2.0-2
    6.12  isabelle_fonts-20190409
    6.13  jdk-11.0.3+7
    6.14 @@ -22,4 +22,4 @@
    6.15  stack-1.9.3
    6.16  vampire-4.2.2
    6.17  xz-java-1.8
    6.18 -z3-4.4.0pre-2
    6.19 +z3-4.4.0pre-3
     7.1 --- a/NEWS	Wed May 22 22:18:45 2019 +0200
     7.2 +++ b/NEWS	Mon May 27 16:47:17 2019 +0200
     7.3 @@ -129,7 +129,7 @@
     7.4  presentation context or to emit markup to the PIDE document. Some
     7.5  predefined markers are taken from the Dublin Core Metadata Initiative,
     7.6  e.g. \<^marker>\<open>contributor arg\<close> or \<^marker>\<open>license arg\<close> and produce PIDE markup that
     7.7 -can retrieved from the document database.
     7.8 +can be retrieved from the document database.
     7.9  
    7.10  * Old-style command tags %name are re-interpreted as markers with
    7.11  proof-scope \<^marker>\<open>tag (proof) name\<close> and produce LaTeX environments as
     8.1 --- a/lib/Tools/update_op	Wed May 22 22:18:45 2019 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,97 +0,0 @@
     8.4 -#!/usr/bin/env bash
     8.5 -#
     8.6 -# Author: Tobias Nipkow, TU Muenchen
     8.7 -#
     8.8 -# DESCRIPTION: update "op _" syntax
     8.9 -
    8.10 -## diagnostics
    8.11 -
    8.12 -function usage()
    8.13 -{
    8.14 -  echo
    8.15 -  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    8.16 -  echo
    8.17 -  echo "  Options are:"
    8.18 -  echo "    -m           ignore .ML files"
    8.19 -  echo
    8.20 -  echo "  Update the old \"op _\" syntax in theory and ML files."
    8.21 -  echo
    8.22 -  exit 1
    8.23 -}
    8.24 -
    8.25 -
    8.26 -IGNORE_ML=""
    8.27 -
    8.28 -while getopts "m" OPT
    8.29 -do
    8.30 -  case "$OPT" in
    8.31 -    m)
    8.32 -      IGNORE_ML="true"
    8.33 -      ;;
    8.34 -    \?)
    8.35 -      usage
    8.36 -      ;;
    8.37 -  esac
    8.38 -done
    8.39 -
    8.40 -shift $(($OPTIND - 1))
    8.41 -
    8.42 -DIR="."
    8.43 -if [ -n "$1" ]; then
    8.44 -  DIR="$1"
    8.45 -fi
    8.46 -
    8.47 -read -r -d '' THY_SCRIPT <<'EOF'
    8.48 -# op [^]\<^bsub>*\<^esub> -> ([^]\<^bsub>*\<^esub>)
    8.49 -s/\([^a-zA-Z0-9_?']\)op [ ]*\(\[\^\]\\<\^bsub>[^\\]*\\<\^esub>\)/\1(\2)/g
    8.50 -# op *XY -> ( *XY)
    8.51 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z][a-zA-Z]\)/\1( \*\2)/g
    8.52 -# op *X -> ( *X)
    8.53 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*\([a-zA-Z]\)/\1( \*\2)/g
    8.54 -# op *R -> ( *R)
    8.55 -s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<^sub>[a-zA-Z]\)/\1( \2)/g
    8.56 -# op *\<cdot> -> ( *\<cdot>)
    8.57 -s/\([^a-zA-Z0-9_?']\)op[ ]*\(\*\\<cdot>\)/\1( \2)/g
    8.58 -# op ** -> ( ** )
    8.59 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*\*/\1( \*\* )/g
    8.60 -# op * -> ( * )
    8.61 -s/\([^a-zA-Z0-9_?']\)op[ ]*\*/\1( \* )/g
    8.62 -# (op +) -> (+)
    8.63 -s/(op [ ]*\([^ )("][^ )(",]*\))/(\1)/g
    8.64 -# (op + -> ((+)
    8.65 -s/(op [ ]*\([^ )(",]*\)\([^)]\)/((\1)\2/g
    8.66 -# op + -> (+)
    8.67 -s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",:]*\)::/\1(\2)::/g
    8.68 -s/\([^a-zA-Z0-9_?']\)op [ ]*\([^ )(",]*\)/\1(\2)/g
    8.69 -# op+ -> (+)
    8.70 -s/\([^a-zA-Z0-9_?']\)op\(\\<[a-zA-Z0-9]*>\)/\1(\2)/g
    8.71 -s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",:]*\)::/\1(\2)::/g
    8.72 -s/\([^a-zA-Z0-9_?']\)op\([^a-zA-Z0-9_? )("\][^ )(",]*\)/\1(\2)/g
    8.73 -EOF
    8.74 -
    8.75 -read -r -d '' ML_SCRIPT <<'EOF'
    8.76 -# op * -> ( * )
    8.77 -s/"\(.*\)\([^a-zA-Z0-9_]\)op[ ]*\*/"\1\2( \* )/g
    8.78 -s/"op[ ]*\*/"( \* )/g
    8.79 -# (op +) -> (+)
    8.80 -s/"\(.*\)(op [ ]*\([^ )("][^ )("]*\))/"\1(\2)/g
    8.81 -s/(op [ ]*\([^ )("][^ )("]*\))\(.*\)"/(\1)\2"/g
    8.82 -# (op + -> ((+)
    8.83 -s/"\(.*\)(op [ ]*\([^ )("]*\)\([^)]\)/"\1((\2)\3/g
    8.84 -# op + -> (+)
    8.85 -s/"\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/"\1\2(\3)/g
    8.86 -s/"op [ ]*\([^ )("]*\)/"(\1)/g
    8.87 -# op+ -> (+)
    8.88 -s/"\(.*\)\([^a-zA-Z0-9_]\)op\([^a-zA-Z0-9_ )("][^ )("]*\)/"\1\2(\3)/g
    8.89 -s/"op\([^a-zA-Z0-9_ )("][^ )("]*\)/"(\1)/g
    8.90 -# is there \<...\> on the line (indicating Isabelle source):
    8.91 -s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op \*/\\<\1>\2\3( * )/g
    8.92 -s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\\<close>/\\<\1>\2\3(\4)\\<close>/g
    8.93 -s/\\<\([^>]*\)>\(.*\)\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)/\\<\1>\2\3(\4)/g
    8.94 -s/\([^a-zA-Z0-9_]\)op [ ]*\([^ )("]*\)\(.*\)\\<\([^>]*\)>/\1(\2)\3\\<\4>/g
    8.95 -EOF
    8.96 -
    8.97 -find "$DIR" -name "*.thy" -exec sed '-i~~' -e "$THY_SCRIPT" {} \;
    8.98 -
    8.99 -[ "$IGNORE_ML" = "true" ] || find "$DIR" -name "*.ML" -exec sed '-i~~' -e "$ML_SCRIPT" {} \;
   8.100 -
     9.1 --- a/src/Doc/JEdit/JEdit.thy	Wed May 22 22:18:45 2019 +0200
     9.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon May 27 16:47:17 2019 +0200
     9.3 @@ -2152,7 +2152,7 @@
     9.4    (by Oracle) on low-quality displays.
     9.5  
     9.6    \<^bold>\<open>Workaround:\<close> Find an old copy of Java 8 from Oracle (which has
     9.7 -  ``end-of-live'' status since Jan-2019) and refer to its main directory via
     9.8 +  ``end-of-life'' status since Jan-2019) and refer to its main directory via
     9.9    @{setting "ISABELLE_JDK_HOME"}\<^verbatim>\<open>="..."\<close> in
    9.10    \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. Also add
    9.11    \<^verbatim>\<open>isabelle_fonts_hinted=false\<close> to
    10.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed May 22 22:18:45 2019 +0200
    10.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Mon May 27 16:47:17 2019 +0200
    10.3 @@ -49,9 +49,9 @@
    10.4  local
    10.5  
    10.6  fun make_command command options problem_path proof_path =
    10.7 -  "(exec 2>&1;" :: map Bash.string (command () @ options) @
    10.8 -  [File.bash_path problem_path, ")", ">", File.bash_path proof_path]
    10.9 -  |> space_implode " "
   10.10 +  Bash.strings (command () @ options) ^ " " ^
   10.11 +    Bash.string (File.platform_path problem_path) ^
   10.12 +    " > " ^ File.bash_path proof_path ^ " 2>&1"
   10.13  
   10.14  fun with_trace ctxt msg f x =
   10.15    let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
    11.1 --- a/src/HOL/Types_To_Sets/unoverload_type.ML	Wed May 22 22:18:45 2019 +0200
    11.2 +++ b/src/HOL/Types_To_Sets/unoverload_type.ML	Mon May 27 16:47:17 2019 +0200
    11.3 @@ -16,7 +16,7 @@
    11.4  fun params_of_class thy class = try (Axclass.get_info thy #> #params) class |> these
    11.5  
    11.6  fun params_of_super_classes thy class =
    11.7 -  Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
    11.8 +  class::Sorts.super_classes (Sign.classes_of thy) class |> maps (params_of_class thy)
    11.9  
   11.10  fun params_of_sort thy sort = maps (params_of_super_classes thy) sort
   11.11  
    12.1 --- a/src/Pure/General/file.ML	Wed May 22 22:18:45 2019 +0200
    12.2 +++ b/src/Pure/General/file.ML	Mon May 27 16:47:17 2019 +0200
    12.3 @@ -50,6 +50,7 @@
    12.4  val bash_path = Bash_Syntax.string o standard_path;
    12.5  val bash_paths = Bash_Syntax.strings o map standard_path;
    12.6  
    12.7 +
    12.8  (* full_path *)
    12.9  
   12.10  fun full_path dir path =
    13.1 --- a/src/Pure/PIDE/document.ML	Wed May 22 22:18:45 2019 +0200
    13.2 +++ b/src/Pure/PIDE/document.ML	Mon May 27 16:47:17 2019 +0200
    13.3 @@ -25,7 +25,7 @@
    13.4    val remove_versions: Document_ID.version list -> state -> state
    13.5    val start_execution: state -> state
    13.6    val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state ->
    13.7 -    Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    13.8 +    string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    13.9    val state: unit -> state
   13.10    val change_state: (state -> state) -> unit
   13.11  end;
   13.12 @@ -294,11 +294,14 @@
   13.13        (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
   13.14        nodes);
   13.15  
   13.16 +fun is_suppressed_node (nodes: node String_Graph.T) (name, node) =
   13.17 +  String_Graph.is_maximal nodes name andalso is_empty_node node;
   13.18 +
   13.19  fun put_node (name, node) (Version nodes) =
   13.20    let
   13.21      val nodes1 = update_node name (K node) nodes;
   13.22      val nodes2 =
   13.23 -      if String_Graph.is_maximal nodes1 name andalso is_empty_node node
   13.24 +      if is_suppressed_node nodes1 (name, node)
   13.25        then String_Graph.del_node name nodes1
   13.26        else nodes1;
   13.27    in Version nodes2 end;
   13.28 @@ -809,7 +812,8 @@
   13.29                              forall (fn (name, (_, node)) => check_theory true name node) imports;
   13.30  
   13.31                          val (print_execs, common, (still_visible, initial)) =
   13.32 -                          if imports_result_changed then (assign_update_empty, NONE, (true, true))
   13.33 +                          if imports_result_changed
   13.34 +                          then (assign_update_empty, NONE, (true, true))
   13.35                            else last_common keywords state node_required node0 node;
   13.36  
   13.37                          val common_command_exec =
   13.38 @@ -865,7 +869,7 @@
   13.39      val state' = state
   13.40        |> define_version new_version_id new_version assigned_nodes;
   13.41  
   13.42 -  in (removed, assign_result, state') end);
   13.43 +  in (Symtab.keys edited, removed, assign_result, state') end);
   13.44  
   13.45  end;
   13.46  
    14.1 --- a/src/Pure/PIDE/document.scala	Wed May 22 22:18:45 2019 +0200
    14.2 +++ b/src/Pure/PIDE/document.scala	Mon May 27 16:47:17 2019 +0200
    14.3 @@ -651,7 +651,7 @@
    14.4      }
    14.5  
    14.6      val init: State =
    14.7 -      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil)._2
    14.8 +      State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2
    14.9    }
   14.10  
   14.11    final case class State private(
   14.12 @@ -768,10 +768,15 @@
   14.13            st <- command_states(version, command).iterator
   14.14          } yield st.exports)
   14.15  
   14.16 -    def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
   14.17 +    def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
   14.18 +      : ((List[Node.Name], List[Command]), State) =
   14.19      {
   14.20        val version = the_version(id)
   14.21  
   14.22 +      val edited_set = edited.toSet
   14.23 +      val edited_nodes =
   14.24 +        (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList
   14.25 +
   14.26        def upd(exec_id: Document_ID.Exec, st: Command.State)
   14.27            : Option[(Document_ID.Exec, Command.State)] =
   14.28          if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st)
   14.29 @@ -794,7 +799,7 @@
   14.30        val new_assignment = the_assignment(version).assign(update)
   14.31        val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
   14.32  
   14.33 -      (changed_commands, new_state)
   14.34 +      ((edited_nodes, changed_commands), new_state)
   14.35      }
   14.36  
   14.37      def is_assigned(version: Version): Boolean =
    15.1 --- a/src/Pure/PIDE/protocol.ML	Wed May 22 22:18:45 2019 +0200
    15.2 +++ b/src/Pure/PIDE/protocol.ML	Mon May 27 16:47:17 2019 +0200
    15.3 @@ -106,7 +106,7 @@
    15.4  
    15.5              val _ = Execution.discontinue ();
    15.6  
    15.7 -            val (removed, assign_update, state') =
    15.8 +            val (edited, removed, assign_update, state') =
    15.9                Document.update old_id new_id edits consolidate state;
   15.10              val _ =
   15.11                (singleton o Future.forks)
   15.12 @@ -117,12 +117,12 @@
   15.13  
   15.14              val _ =
   15.15                Output.protocol_message Markup.assign_update
   15.16 -                ((new_id, assign_update) |>
   15.17 +                ((new_id, edited, assign_update) |>
   15.18                    let
   15.19                      open XML.Encode;
   15.20                      fun encode_upd (a, bs) =
   15.21                        string (space_implode "," (map Value.print_int (a :: bs)));
   15.22 -                  in pair int (list encode_upd) end
   15.23 +                  in triple int (list string) (list encode_upd) end
   15.24                    |> YXML.chunks_of_body);
   15.25            in Document.start_execution state' end)));
   15.26  
    16.1 --- a/src/Pure/PIDE/protocol.scala	Wed May 22 22:18:45 2019 +0200
    16.2 +++ b/src/Pure/PIDE/protocol.scala	Mon May 27 16:47:17 2019 +0200
    16.3 @@ -13,7 +13,9 @@
    16.4  
    16.5    object Assign_Update
    16.6    {
    16.7 -    def unapply(text: String): Option[(Document_ID.Version, Document.Assign_Update)] =
    16.8 +    def unapply(text: String)
    16.9 +      : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
   16.10 +    {
   16.11        try {
   16.12          import XML.Decode._
   16.13          def decode_upd(body: XML.Body): (Long, List[Long]) =
   16.14 @@ -21,12 +23,13 @@
   16.15              case a :: bs => (a, bs)
   16.16              case _ => throw new XML.XML_Body(body)
   16.17            }
   16.18 -        Some(pair(long, list(decode_upd _))(Symbol.decode_yxml(text)))
   16.19 +        Some(triple(long, list(string), list(decode_upd _))(Symbol.decode_yxml(text)))
   16.20        }
   16.21        catch {
   16.22          case ERROR(_) => None
   16.23          case _: XML.Error => None
   16.24        }
   16.25 +    }
   16.26    }
   16.27  
   16.28    object Removed
    17.1 --- a/src/Pure/PIDE/session.scala	Wed May 22 22:18:45 2019 +0200
    17.2 +++ b/src/Pure/PIDE/session.scala	Mon May 27 16:47:17 2019 +0200
    17.3 @@ -269,15 +269,19 @@
    17.4      }
    17.5      private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
    17.6  
    17.7 -    def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
    17.8 -      assignment |= assign
    17.9 -      for (command <- cmds) {
   17.10 -        nodes += command.node_name
   17.11 -        command.blobs_names.foreach(nodes += _)
   17.12 -        commands += command
   17.13 +    def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
   17.14 +      synchronized {
   17.15 +        assignment |= assign
   17.16 +        for (node <- edited_nodes) {
   17.17 +          nodes += node
   17.18 +        }
   17.19 +        for (command <- cmds) {
   17.20 +          nodes += command.node_name
   17.21 +          command.blobs_names.foreach(nodes += _)
   17.22 +          commands += command
   17.23 +        }
   17.24 +        delay_flush.invoke()
   17.25        }
   17.26 -      delay_flush.invoke()
   17.27 -    }
   17.28  
   17.29      def shutdown()
   17.30      {
   17.31 @@ -457,7 +461,7 @@
   17.32        {
   17.33          try {
   17.34            val st = global_state.change_result(f)
   17.35 -          change_buffer.invoke(false, List(st.command))
   17.36 +          change_buffer.invoke(false, Nil, List(st.command))
   17.37          }
   17.38          catch { case _: Document.State.Fail => bad_output() }
   17.39        }
   17.40 @@ -485,10 +489,11 @@
   17.41  
   17.42                case Markup.Assign_Update =>
   17.43                  msg.text match {
   17.44 -                  case Protocol.Assign_Update(id, update) =>
   17.45 +                  case Protocol.Assign_Update(id, edited, update) =>
   17.46                      try {
   17.47 -                      val cmds = global_state.change_result(_.assign(id, update))
   17.48 -                      change_buffer.invoke(true, cmds)
   17.49 +                      val (edited_nodes, cmds) =
   17.50 +                        global_state.change_result(_.assign(id, edited, update))
   17.51 +                      change_buffer.invoke(true, edited_nodes, cmds)
   17.52                        manager.send(Session.Change_Flush)
   17.53                      }
   17.54                      catch { case _: Document.State.Fail => bad_output() }
    18.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed May 22 22:18:45 2019 +0200
    18.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon May 27 16:47:17 2019 +0200
    18.3 @@ -48,7 +48,7 @@
    18.4      val state1 =
    18.5        state0.continue_history(Future.value(version0), edits, Future.value(version1))
    18.6          .define_version(version1, state0.the_assignment(version0))
    18.7 -        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
    18.8 +        .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
    18.9  
   18.10      (command.source, state1)
   18.11    }
    19.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Wed May 22 22:18:45 2019 +0200
    19.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Mon May 27 16:47:17 2019 +0200
    19.3 @@ -92,7 +92,7 @@
    19.4      private val query_label = new Label("Find:") {
    19.5        tooltip =
    19.6          GUI.tooltip_lines(
    19.7 -          "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
    19.8 +          "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
    19.9      }
   19.10  
   19.11      val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)