--- a/Admin/components/PLATFORMS Tue Oct 03 15:01:54 2023 +0100
+++ b/Admin/components/PLATFORMS Wed Oct 11 14:25:14 2023 +0100
@@ -41,10 +41,12 @@
macOS 11 Big Sur (mini1 Macmini8,1)
macOS 12 Monterey (laramac01 Macmini8,1)
macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2 Pro, 6+4 cores)
+ macOS 14 Sonoma (???)
arm64-darwin macOS 11 Big Sur (assur Macmini9,1 -- MacMini M1, 4+4 cores)
macOS 12 Monterey (???)
macOS 13 Ventura (mini3 Mac14,12 -- MacMini M2 Pro, 6+4 cores)
+ macOS 14 Sonoma (???)
x86_64-windows Windows 10
x86_64-cygwin Cygwin 3.4.x https://isabelle.sketis.net/cygwin_2023 (x86_64/release)
--- a/Admin/components/components.sha1 Tue Oct 03 15:01:54 2023 +0100
+++ b/Admin/components/components.sha1 Wed Oct 11 14:25:14 2023 +0100
@@ -115,6 +115,7 @@
71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz
c489cae2a96ce18bec813d2eb1f528c88006382a go-1.21.0-v1.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
+c947c751810777a4a7668d1b1b92942f178bb7b5 hugo-0.119.0.tar.gz
511fa8df8be88eb0500032bbd17742d33bdd4636 hugo-0.88.1.tar.gz
989234b3799fe8750f3c24825d1f717c24fb0214 idea-icons-20210508.tar.gz
20b53cfc3ffc5b15c1eabc91846915b49b4c0367 isabelle_fonts-20151021.tar.gz
--- a/etc/build.props Tue Oct 03 15:01:54 2023 +0100
+++ b/etc/build.props Wed Oct 11 14:25:14 2023 +0100
@@ -26,6 +26,7 @@
src/Pure/Admin/component_eptcs.scala \
src/Pure/Admin/component_foiltex.scala \
src/Pure/Admin/component_fonts.scala \
+ src/Pure/Admin/component_hugo.scala \
src/Pure/Admin/component_jdk.scala \
src/Pure/Admin/component_jedit.scala \
src/Pure/Admin/component_jsoup.scala \
--- a/src/Doc/Implementation/ML.thy Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Doc/Implementation/ML.thy Wed Oct 11 14:25:14 2023 +0100
@@ -1070,8 +1070,13 @@
text \<open>
The Standard ML semantics of strict functional evaluation together with
- exceptions is rather well defined, but some delicate points need to be
- observed to avoid that ML programs go wrong despite static type-checking.
+ exceptions is rather well defined, but some fine points need to be observed
+ to avoid that ML programs go wrong despite static type-checking.
+
+ Unlike official Standard ML, Isabelle/ML rejects catch-all patterns in
+ \<^ML_text>\<open>handle\<close> clauses: this improves the robustness of ML programs,
+ especially against arbitrary physical events (interrupts).
+
Exceptions in Isabelle/ML are subsequently categorized as follows.
\<close>
@@ -1100,14 +1105,15 @@
paragraph \<open>Program failures.\<close>
text \<open>
There is a handful of standard exceptions that indicate general failure
- situations, or failures of core operations on logical entities (types,
- terms, theorems, theories, see \chref{ch:logic}).
+ situations (e.g.\ \<^ML>\<open>Fail\<close>), or failures of core operations on logical
+ entities (types, terms, theorems, theories, see \chref{ch:logic}).
These exceptions indicate a genuine breakdown of the program, so the main
- purpose is to determine quickly what has happened where. Traditionally, the
- (short) exception message would include the name of an ML function, although
- this is no longer necessary, because the ML runtime system attaches detailed
- source position stemming from the corresponding \<^ML_text>\<open>raise\<close> keyword.
+ purpose is to determine quickly what has happened in the ML program.
+ Traditionally, the (short) exception message would include the name of an ML
+ function, although this is not strictly necessary, because the ML runtime
+ system attaches detailed source position stemming from the corresponding
+ \<^ML_text>\<open>raise\<close> keyword.
\<^medskip>
User modules can always introduce their own custom exceptions locally, e.g.\
@@ -1120,32 +1126,31 @@
paragraph \<open>Interrupts.\<close>
text \<open>
These indicate arbitrary system events: both the ML runtime system and the
- Isabelle/ML infrastructure signal various exceptional situations by raising
- special exceptions user code, satisfying the predicate
+ Isabelle/ML infrastructure may signal various exceptional situations by
+ raising special exceptions user code, satisfying the predicate
\<^ML>\<open>Exn.is_interrupt\<close>.
This is the one and only way that physical events can intrude an Isabelle/ML
program. Such an interrupt can mean out-of-memory, stack overflow, timeout,
internal signaling of threads, or a POSIX process signal. An Isabelle/ML
program that intercepts interrupts becomes dependent on physical effects of
- the environment. Even worse, exception handling patterns that are too
- general by accident, e.g.\ by misspelled exception constructors, will cover
- interrupts unintentionally and thus render the program semantics
- ill-defined.
-
- Note that the Interrupt exception dates back to the original SML90 language
- definition. It was excluded from the SML97 version to avoid its malign
- impact on ML program semantics, but without providing a viable alternative.
- Isabelle/ML recovers physical interruptibility (which is an indispensable
- tool to implement managed evaluation of command transactions), but requires
- user code to be strictly transparent wrt.\ interrupts.
-
- \begin{warn}
- Isabelle/ML user code needs to terminate promptly on interruption, without
- guessing at its meaning to the system infrastructure. Temporary handling of
- interrupts for cleanup of global resources etc.\ needs to be followed
- immediately by re-raising of the original exception.
- \end{warn}
+ the environment (e.g.\ via \<^ML>\<open>Exn.capture\<close> without subsequent
+ \<^ML>\<open>Exn.release\<close>).
+
+ Note that the original SML90 language had an \<^verbatim>\<open>Interrupt\<close> exception, but
+ that was excluded from SML97 to simplify ML the mathematical semantics.
+ Isabelle/ML does support physical interrupts thanks to special features of
+ the underlying Poly/ML compiler and runtime system. This works robustly,
+ because the old \<^ML_text>\<open>Interrupt\<close> constructor has been removed from the
+ ML environment, and catch-all patterns \<^ML_text>\<open>handle\<close> are rejected.
+ Thus user code becomes strictly transparent wrt.\ interrupts: physical
+ events are exposed to the toplevel, and the mathematical meaning of the
+ program becomes a partial function that is otherwise unchanged.
+
+ The Isabelle/ML antiquotation @{ML_antiquotation try}, with its syntactic
+ variants for \<^ML_text>\<open>catch\<close> or \<^ML_text>\<open>finally\<close>, supports
+ intermediate handling of interrupts and subsequent cleanup-operations,
+ without swallowing such physical event.
\<close>
text %mlref \<open>
@@ -1159,15 +1164,11 @@
@{define_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
\end{mldecls}
- \<^rail>\<open>
- (@@{ML_antiquotation try} | @@{ML_antiquotation can}) embedded
- \<close>
-
- \<^descr> \<^ML>\<open>try\<close>~\<open>f x\<close> makes the partiality of evaluating \<open>f x\<close> explicit via the
- option datatype. Interrupts are \<^emph>\<open>not\<close> handled here, i.e.\ this form serves
- as safe replacement for the \<^emph>\<open>unsafe\<close> version \<^ML_text>\<open>(SOME\<close>~\<open>f
+ \<^descr> \<^ML>\<open>try\<close>~\<open>f x\<close> makes the partiality of evaluating \<open>f x\<close> explicit via
+ the option datatype. Interrupts are \<^emph>\<open>not\<close> handled here, i.e.\ this form
+ serves as safe replacement for the \<^emph>\<open>fragile\<close> version \<^ML_text>\<open>(SOME\<close>~\<open>f
x\<close>~\<^ML_text>\<open>handle _ => NONE)\<close> that is occasionally seen in books about
- SML97, but not in Isabelle/ML.
+ SML97.
\<^descr> \<^ML>\<open>can\<close> is similar to \<^ML>\<open>try\<close> with more abstract result.
@@ -1175,11 +1176,13 @@
raised indirectly via the \<^ML>\<open>error\<close> function (see
\secref{sec:message-channels}).
- \<^descr> \<^ML>\<open>Fail\<close>~\<open>msg\<close> represents general program failures.
-
- \<^descr> \<^ML>\<open>Exn.is_interrupt\<close> identifies interrupts robustly, without mentioning
- concrete exception constructors in user code. Handled interrupts need to be
- re-raised promptly!
+ \<^descr> \<^ML>\<open>Fail\<close>~\<open>msg\<close> represents general program failures, but not user errors.
+
+ \<^descr> \<^ML>\<open>Exn.is_interrupt\<close> identifies interrupts, without mentioning
+ concrete exception constructors in user code. Since \<^ML_text>\<open>handle\<close> with
+ catch-all patterns is rejected, it cannot handle interrupts at all. In the
+ rare situations where this is really required, use \<^ML>\<open>Exn.capture\<close> and
+ \<^ML>\<open>Exn.release\<close> (\secref{sec:managed-eval}).
\<^descr> \<^ML>\<open>Exn.reraise\<close>~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
position information (if possible, depending on the ML platform).
@@ -1200,9 +1203,45 @@
@{ML_antiquotation_def "undefined"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
- \<^descr> \<open>@{try}\<close> and \<open>{can}\<close> are similar to the corresponding functions, but the
- argument is taken directly as ML expression: functional abstraction and
- application is done implicitly.
+ \<^rail>\<open>
+ (@@{ML_antiquotation try} | @@{ML_antiquotation can}) embedded
+ \<close>
+
+
+ \<^descr> \<open>@{try}\<close> and \<open>{can}\<close> take embedded ML source as arguments, and modify the
+ evaluation analogously to the combinators \<^ML>\<open>try\<close> and \<^ML>\<open>can\<close> above,
+ but with special treatment of the interrupt state of the underlying ML
+ thread. There are also variants to support \<^verbatim>\<open>try_catch\<close> and \<^verbatim>\<open>try_finally\<close>
+ blocks similar to Scala.
+
+ The substructure of the embedded argument supports the following syntax
+ variants:
+
+ \<^rail>\<open>
+ @{syntax_def try_catch}: @{syntax expr} @'catch' @{syntax handler};
+ @{syntax_def try_finally}: @{syntax expr} @'finally' @{syntax cleanup};
+ @{syntax_def try}: @{syntax expr};
+ @{syntax_def can}: @{syntax expr}
+ \<close>
+
+ The @{syntax handler} of \<^verbatim>\<open>try_catch\<close> follows the syntax of \<^ML_text>\<open>fn\<close>
+ patterns, so it is similar to \<^ML_text>\<open>handle\<close>: the key difference is
+ that interrupts are always passed-through via \<^ML>\<open>Exn.reraise\<close>.
+
+ The @{syntax cleanup} expression of \<^verbatim>\<open>try_finally\<close> is always invoked,
+ regardless of the overall exception result, and afterwards exceptions are
+ passed-through via \<^ML>\<open>Exn.reraise\<close>.
+
+ Both the @{syntax handler} and @{syntax cleanup} are evaluated with further
+ interrupts disabled! These expressions should terminate promptly; timeouts
+ don't work here.
+
+ \<^medskip>
+ Implementation details can be seen in \<^ML>\<open>Isabelle_Thread.try_catch\<close>,
+ \<^ML>\<open>Isabelle_Thread.try_finally\<close>, \<^ML>\<open>Isabelle_Thread.try\<close>, and
+ \<^ML>\<open>Isabelle_Thread.can\<close>, respectively. The ML antiquotations add
+ functional abstractions as required for these ``special forms'' of
+ Isabelle/ML.
\<^descr> \<open>@{assert}\<close> inlines a function \<^ML_type>\<open>bool -> unit\<close> that raises
\<^ML>\<open>Fail\<close> if the argument is \<^ML>\<open>false\<close>. Due to inlining the source
@@ -1213,16 +1252,21 @@
\<close>
text %mlex \<open>
- We define a total version of division: any failures are swept under the
+
+ We define total versions of division: any failures are swept under the
carpet and mapped to a default value. Thus division-by-zero becomes 0, but
- there could be other exceptions like overflow that produce the same result
- (for unbounded integers this does not happen).
+ there could be other exceptions like overflow that produce the same result.
+
+ For unbounded integers such side-errors do not happen, but it might still be
+ better to be explicit about exception patterns (second version below).
\<close>
ML \<open>
- fun div_total x y = \<^try>\<open>x div y\<close> |> the_default 0;
-
- \<^assert> (div_total 1 0 = 0);
+ fun div_total1 x y = \<^try>\<open>x div y catch _ => 0\<close>;
+ fun div_total2 x y = \<^try>\<open>x div y catch Div => 0\<close>;
+
+ \<^assert> (div_total1 1 0 = 0);
+ \<^assert> (div_total2 1 0 = 0);
\<close>
text \<open>
@@ -1238,7 +1282,7 @@
instead:
\<close>
-ML \<open>fun undefined _ = \<^undefined>\<close>
+ML \<open>fun undefined _ = @{undefined}\<close>
text \<open>
\<^medskip>
@@ -1249,8 +1293,9 @@
ML \<open>fun undefined _ = \<^undefined>\<close>
text \<open>
- \<^medskip> Semantically, all forms are equivalent to a function definition
- without any clauses, but that is syntactically not allowed in ML.
+ \<^medskip>
+ Semantically, all forms are equivalent to a function definition without any
+ clauses, but that is syntactically not allowed in ML.
\<close>
@@ -1908,7 +1953,7 @@
\<close>
-section \<open>Managed evaluation\<close>
+section \<open>Managed evaluation \label{sec:managed-eval}\<close>
text \<open>
Execution of Standard ML follows the model of strict functional evaluation
--- a/src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.thy Tue Oct 03 15:01:54 2023 +0100
+++ b/src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.thy Wed Oct 11 14:25:14 2023 +0100
@@ -13,26 +13,4 @@
sledgehammer_params [verit, isar_proof, minimize = false, slices = 1, compress = 1]
-lemma
- fixes a b c :: int
- shows "a + b = c \<Longrightarrow> c - b = a"
- sledgehammer [expect = some_preplayed] ()
-proof -
- assume a1: "a + b = c"
- have "c - b \<le> a \<or> c \<noteq> a + b"
- by force
- then have f2: "c - b \<le> a"
- using a1 by force
- have "a \<le> c - b \<or> c \<noteq> a + b"
- by force
- then have "a \<le> c - b"
- using a1 by force
- then have f3: "c - b \<le> a \<and> a \<le> c - b"
- using f2 by fastforce
- have "c - b = a \<or> \<not> c - b \<le> a \<or> \<not> a \<le> c - b"
- by auto
- then show ?thesis
- using f3 by meson
-qed
-
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/component_hugo.scala Wed Oct 11 14:25:14 2023 +0100
@@ -0,0 +1,123 @@
+/* Title: Pure/Admin/component_hugo.scala
+ Author: Fabian Huch, TU Muenchen
+
+Build Isabelle component for hugo site generator. See also:
+
+ - https://gohugo.io
+ - https://github.com/gohugoio/hugo
+*/
+
+package isabelle
+
+
+object Component_Hugo {
+ /* platform information */
+
+ sealed case class Download_Platform(platform_name: String, url_template: String) {
+ override def toString: String = platform_name
+
+ def is_windows: Boolean = url_template.contains("windows")
+ def url(base_url: String, version: String): String =
+ base_url + "/v" + version + "/" + url_template.replace("{V}", version)
+ }
+
+ val platforms: List[Download_Platform] =
+ List(
+ Download_Platform("arm64-darwin", "hugo_extended_{V}_darwin-universal.tar.gz"),
+ Download_Platform("arm64-linux", "hugo_extended_{V}_linux-arm64.tar.gz"),
+ Download_Platform("x86_64-darwin", "hugo_extended_{V}_darwin-universal.tar.gz"),
+ Download_Platform("x86_64-linux", "hugo_extended_{V}_linux-amd64.tar.gz"),
+ Download_Platform("x86_64-windows", "hugo_extended_{V}_windows-amd64.zip"))
+
+
+ /* build hugo */
+
+ val default_url = "https://github.com/gohugoio/hugo/releases/download"
+ val default_version = "0.119.0"
+
+ def build_hugo(
+ base_url: String = default_url,
+ version: String = default_version,
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress
+ ): Unit = {
+ /* component */
+
+ val component = "hugo-" + version
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
+
+
+ /* download */
+
+ for (platform <- platforms) {
+ val platform_dir =
+ Isabelle_System.make_directory(component_dir.path + Path.basic(platform.platform_name))
+
+ val url = platform.url(base_url, version)
+ val name = Library.take_suffix(_ != '/', url.toList)._2.mkString
+
+ val exe = Path.basic("hugo").exe_if(platform.is_windows)
+
+ Isabelle_System.with_tmp_dir("download", component_dir.path.file) { download_dir =>
+ Isabelle_System.with_tmp_dir("tmp", component_dir.path.file) { tmp_dir =>
+ val archive_file = download_dir + Path.basic(name)
+
+ Isabelle_System.download_file(url, archive_file, progress = progress)
+ Isabelle_System.extract(archive_file, tmp_dir)
+ Isabelle_System.move_file(tmp_dir + exe, platform_dir)
+ Isabelle_System.move_file(tmp_dir + Path.basic("LICENSE"), component_dir.LICENSE)
+ File.set_executable(platform_dir + exe)
+ }
+ }
+ }
+
+
+ /* settings */
+
+ component_dir.write_settings("""
+ISABELLE_HUGO="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
+""")
+
+
+ /* README */
+
+ File.write(component_dir.README,
+ """This Isabelle components provides a hugo extended """ + version + """.
+
+See also https://gohugo.io and executables from """ + base_url + """
+
+ Fabian
+ """ + Date.Format.date(Date.now()) + "\n")
+ }
+
+ val isabelle_tool =
+ Isabelle_Tool("component_hugo", "build hugo component", Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var base_url = default_url
+ var version = default_version
+
+ val getopts = Getopts("""
+Usage: isabelle component_hugo [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -U URL download URL (default: """" + default_url + """")
+ -V VERSION version (default: """" + default_version + """")
+
+ Build extended hugo component.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => base_url = arg),
+ "V:" -> (arg => version = arg))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_hugo(base_url = base_url, version = version, target_dir = target_dir,
+ progress = progress)
+ })
+}
--- a/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 11 14:25:14 2023 +0100
@@ -339,14 +339,17 @@
" -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
- args = "-a -d '~~/src/Benchmarks'"),
+ args = "-a -d '~~/src/Benchmarks'",
+ active = () => false),
Remote_Build("macOS, quick_and_dirty", "mini2",
options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
args = "-a -o quick_and_dirty",
- detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")),
+ detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"),
+ active = () => false),
Remote_Build("macOS, skip_proofs", "mini2",
options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
- detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))),
+ detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
+ active = () => false)),
List(
Remote_Build("macOS 13 Ventura (ARM64)", "mini3",
history_base = "8e590adaac5e",
--- a/src/Pure/Concurrent/isabelle_thread.ML Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.ML Wed Oct 11 14:25:14 2023 +0100
@@ -27,7 +27,7 @@
val interrupt_other: T -> unit
structure Exn: EXN
val expose_interrupt_result: unit -> unit Exn.result
- val expose_interrupt: unit -> unit (*exception Interrupt*)
+ val expose_interrupt: unit -> unit (*exception Exn.is_interrupt*)
val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
val try: (unit -> 'a) -> 'a option
--- a/src/Pure/ML/ml_init.ML Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Pure/ML/ml_init.ML Wed Oct 11 14:25:14 2023 +0100
@@ -8,7 +8,7 @@
val _ =
List.app ML_Name_Space.forget_val
- ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
+ ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat", "Interrupt"];
val ord = SML90.ord;
val chr = SML90.chr;
@@ -19,8 +19,6 @@
val error_depth = PolyML.error_depth;
-datatype illegal = Interrupt;
-
structure Basic_Exn: BASIC_EXN = Exn;
open Basic_Exn;
--- a/src/Pure/Pure.thy Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Pure/Pure.thy Wed Oct 11 14:25:14 2023 +0100
@@ -1559,5 +1559,6 @@
declare [[ML_write_global = false]]
ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>
+ML_command \<open>\<^assert> (not (can ML_command \<open>() handle Interrupt => ()\<close>))\<close>
end
--- a/src/Pure/System/isabelle_tool.scala Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Pure/System/isabelle_tool.scala Wed Oct 11 14:25:14 2023 +0100
@@ -170,6 +170,7 @@
Component_Easychair.isabelle_tool,
Component_Foiltex.isabelle_tool,
Component_Fonts.isabelle_tool,
+ Component_Hugo.isabelle_tool,
Component_JDK.isabelle_tool,
Component_JEdit.isabelle_tool,
Component_Jsoup.isabelle_tool,
--- a/src/Pure/Tools/scala_project.scala Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Pure/Tools/scala_project.scala Wed Oct 11 14:25:14 2023 +0100
@@ -12,7 +12,7 @@
/** build tools **/
val java_version: String = "17"
- val scala_version: String = "3.1.3"
+ val scala_version: String = "3.3.0"
abstract class Build_Tool {
def project_root: Path
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Tue Oct 03 15:01:54 2023 +0100
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala Wed Oct 11 14:25:14 2023 +0100
@@ -176,7 +176,8 @@
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = {
val opt_snapshot =
Document_Model.get_model(buffer) match {
- case Some(model) if model.is_theory => Some(Document_Model.snapshot(model))
+ case Some(model) if model.is_theory =>
+ GUI_Thread.now { Some(Document_Model.snapshot(model)) }
case _ => None
}
opt_snapshot match {