# HG changeset patch # User wenzelm # Date 1664217637 -7200 # Node ID 2802f6a4dd8bc5a847a5e69ac622553bfb1d0d4f # Parent 14dd8b46307f45e73262a3a6a13306f636d7b97f# Parent e44e044dadb3aa90974246c2bbcc077bff543c8e merged diff -r 14dd8b46307f -r 2802f6a4dd8b lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty Mon Sep 26 08:41:53 2022 +0000 +++ b/lib/texinputs/isabellesym.sty Mon Sep 26 20:40:37 2022 +0200 @@ -480,6 +480,7 @@ \newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} \newcommand{\isactrltvar}{\isakeywordcontrol{tvar}} \newcommand{\isactrlvar}{\isakeywordcontrol{var}} +\newcommand{\isactrlverbatim}{\isakeywordcontrol{verbatim}} \newcommand{\isactrlConst}{\isakeywordcontrol{Const}} \newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}} \newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}} diff -r 14dd8b46307f -r 2802f6a4dd8b src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Sep 26 08:41:53 2022 +0000 +++ b/src/Pure/Tools/build.scala Mon Sep 26 20:40:37 2022 +0200 @@ -138,6 +138,7 @@ class Results private[Build]( val store: Sessions.Store, + val deps: Sessions.Deps, results: Map[String, (Option[Process_Result], Sessions.Info)], val presentation_sessions: List[String] ) { @@ -464,7 +465,7 @@ if result.ok && browser_info.enabled(result.info) } yield name).toList - new Results(store, results, presentation_sessions) + new Results(store, build_deps, results, presentation_sessions) } if (export_files) { @@ -483,7 +484,7 @@ } if (results.presentation_sessions.nonEmpty && !progress.stopped) { - Browser_Info.build(browser_info, store, build_deps, results.presentation_sessions, + Browser_Info.build(browser_info, results.store, results.deps, results.presentation_sessions, progress = progress, verbose = verbose) }