--- a/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 01 12:43:39 2023 +0000
+++ b/src/HOL/BNF_Cardinal_Order_Relation.thy Wed Feb 01 21:29:35 2023 +0100
@@ -759,7 +759,7 @@
theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product
does not increase cardinality -- the proof of this fact adapts a standard
set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
-at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
+at page 47 in \<^cite>\<open>"card-book"\<close>. Then everything else follows fairly easily.\<close>
lemma infinite_iff_card_of_nat:
"\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
--- a/src/HOL/Binomial.thy Wed Feb 01 12:43:39 2023 +0000
+++ b/src/HOL/Binomial.thy Wed Feb 01 21:29:35 2023 +0100
@@ -718,7 +718,7 @@
using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
-text \<open>The absorption identity (equation 5.5 @{cite \<open>p.~157\<close> GKP_CM}):
+text \<open>The absorption identity (equation 5.5 \<^cite>\<open>\<open>p.~157\<close> in GKP_CM\<close>):
\[
{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
\]\<close>
@@ -728,7 +728,7 @@
text \<open>The absorption identity is written in the following form to avoid
division by $k$ (the lower index) and therefore remove the $k \neq 0$
-restriction @{cite \<open>p.~157\<close> GKP_CM}:
+restriction \<^cite>\<open>\<open>p.~157\<close> in GKP_CM\<close>:
\[
k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
\]\<close>
@@ -740,7 +740,7 @@
by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)
text \<open>The absorption companion identity for natural number coefficients,
- following the proof by GKP @{cite \<open>p.~157\<close> GKP_CM}:\<close>
+ following the proof by GKP \<^cite>\<open>\<open>p.~157\<close> in GKP_CM\<close>:\<close>
lemma binomial_absorb_comp: "(n - k) * (n choose k) = n * ((n - 1) choose k)"
(is "?lhs = ?rhs")
proof (cases "n \<le> k")
@@ -771,7 +771,7 @@
by (subst choose_reduce_nat) simp_all
text \<open>
- Equation 5.9 of the reference material @{cite \<open>p.~159\<close> GKP_CM} is a useful
+ Equation 5.9 of the reference material \<^cite>\<open>\<open>p.~159\<close> in GKP_CM\<close> is a useful
summation formula, operating on both indices:
\[
\sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
@@ -793,7 +793,7 @@
subsubsection \<open>Summation on the upper index\<close>
text \<open>
- Another summation formula is equation 5.10 of the reference material @{cite \<open>p.~160\<close> GKP_CM},
+ Another summation formula is equation 5.10 of the reference material \<^cite>\<open>\<open>p.~160\<close> in GKP_CM\<close>,
aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} =
{n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
\<close>
--- a/src/HOL/GCD.thy Wed Feb 01 12:43:39 2023 +0000
+++ b/src/HOL/GCD.thy Wed Feb 01 21:29:35 2023 +0100
@@ -2011,7 +2011,7 @@
lemma gcd_mult_distrib_nat: "k * gcd m n = gcd (k * m) (k * n)"
for k m n :: nat
- \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
+ \<comment> \<open>\<^cite>\<open>\<open>page 27\<close> in davenport92\<close>\<close>
by (simp add: gcd_mult_left)
lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
--- a/src/HOL/HOL.thy Wed Feb 01 12:43:39 2023 +0000
+++ b/src/HOL/HOL.thy Wed Feb 01 21:29:35 2023 +0100
@@ -57,7 +57,7 @@
subsection \<open>Primitive logic\<close>
text \<open>
-The definition of the logic is based on Mike Gordon's technical report @{cite "Gordon-TR68"} that
+The definition of the logic is based on Mike Gordon's technical report \<^cite>\<open>"Gordon-TR68"\<close> that
describes the first implementation of HOL. However, there are a number of differences.
In particular, we start with the definite description operator and introduce Hilbert's \<open>\<epsilon>\<close> operator
only much later. Moreover, axiom \<open>(P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P) \<longrightarrow> (P = Q)\<close> is derived from the other
--- a/src/HOL/Wellfounded.thy Wed Feb 01 12:43:39 2023 +0000
+++ b/src/HOL/Wellfounded.thy Wed Feb 01 21:29:35 2023 +0100
@@ -617,7 +617,7 @@
text \<open>
Inductive definition of the accessible part \<open>acc r\<close> of a
- relation; see also @{cite "paulin-tlca"}.
+ relation; see also \<^cite>\<open>"paulin-tlca"\<close>.
\<close>
inductive_set acc :: "('a \<times> 'a) set \<Rightarrow> 'a set" for r :: "('a \<times> 'a) set"
--- a/src/Pure/Admin/isabelle_cronjob.scala Wed Feb 01 12:43:39 2023 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Feb 01 21:29:35 2023 +0100
@@ -376,7 +376,7 @@
List(
Remote_Build("AFP", "lrzcloud2",
java_heap = "8g",
- options = "-m32 -M1x6 -t AFP" +
+ options = "-m32 -M1x5 -t AFP" +
" -e ISABELLE_GHC=ghc" +
" -e ISABELLE_MLTON=mlton -e ISABELLE_MLTON_OPTIONS=" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
--- a/src/Pure/PIDE/headless.scala Wed Feb 01 12:43:39 2023 +0000
+++ b/src/Pure/PIDE/headless.scala Wed Feb 01 21:29:35 2023 +0100
@@ -647,8 +647,7 @@
if (!node_name.is_theory) error("Not a theory file: " + path)
progress.expose_interrupt()
- val text0 = File.read(path)
- val text = if (unicode_symbols) Symbol.decode(text0) else text0
+ val text = Symbol.output(unicode_symbols, File.read(path))
val node_header = resources.check_thy(node_name, Scan.char_reader(text))
new Resources.Theory(node_name, node_header, text, true)
}
--- a/src/Pure/System/progress.scala Wed Feb 01 12:43:39 2023 +0000
+++ b/src/Pure/System/progress.scala Wed Feb 01 21:29:35 2023 +0100
@@ -85,7 +85,7 @@
/* structured program progress */
object Program_Progress {
- class Program private[Program_Progress](title: String) {
+ class Program private[Program_Progress](heading: String, title: String) {
private val output_buffer = new StringBuffer(256) // synchronized
def echo(msg: String): Unit = synchronized {
@@ -97,7 +97,7 @@
private var stop_time: Option[Time] = None
def stop_now(): Unit = synchronized { stop_time = Some(Time.now()) }
- def output(heading: String): (Command.Results, XML.Body) = synchronized {
+ def output(): (Command.Results, XML.Body) = synchronized {
val output_text = output_buffer.toString
val elapsed_time = stop_time.map(t => t - start_time)
@@ -127,20 +127,23 @@
}
}
-abstract class Program_Progress(default_program: String = "program") extends Progress {
+abstract class Program_Progress(
+ default_heading: String = "Running",
+ default_title: String = "program"
+) extends Progress {
private var _finished_programs: List[Program_Progress.Program] = Nil
private var _running_program: Option[Program_Progress.Program] = None
- def output(heading: String = "Running"): (Command.Results, XML.Body) = synchronized {
+ def output(): (Command.Results, XML.Body) = synchronized {
val programs = (_running_program.toList ::: _finished_programs).reverse
- val programs_output = programs.map(_.output(heading))
+ val programs_output = programs.map(_.output())
val results = Command.Results.merge(programs_output.map(_._1))
val body = Library.separate(Pretty.Separator, programs_output.map(_._2)).flatten
(results, body)
}
- private def start_program(title: String): Unit = synchronized {
- _running_program = Some(new Program_Progress.Program(title))
+ private def start_program(heading: String, title: String): Unit = synchronized {
+ _running_program = Some(new Program_Progress.Program(heading, title))
}
def stop_program(): Unit = synchronized {
@@ -156,12 +159,12 @@
def detect_program(s: String): Option[String]
override def echo(msg: String): Unit = synchronized {
- detect_program(msg) match {
- case Some(title) =>
+ detect_program(msg).map(Word.explode) match {
+ case Some(a :: bs) =>
stop_program()
- start_program(title)
- case None =>
- if (_running_program.isEmpty) start_program(default_program)
+ start_program(a, Word.implode(bs))
+ case _ =>
+ if (_running_program.isEmpty) start_program(default_heading, default_title)
_running_program.get.echo(msg)
}
}
--- a/src/Pure/Thy/document_build.scala Wed Feb 01 12:43:39 2023 +0000
+++ b/src/Pure/Thy/document_build.scala Wed Feb 01 21:29:35 2023 +0100
@@ -132,12 +132,15 @@
List("isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
map(name => texinputs + Path.basic(name))
- def running_script(title: String): String =
- "echo " + Bash.string("Running program \"" + title + "\" ...") + ";"
+ def program_start(title: String): String =
+ "PROGRAM START \"" + title + "\" ..."
- def detect_running_script(s: String): Option[String] =
+ def program_running_script(title: String): String =
+ "echo " + Bash.string(program_start("Running " + title)) + ";"
+
+ def detect_program_start(s: String): Option[String] =
for {
- s1 <- Library.try_unprefix("Running program \"", s)
+ s1 <- Library.try_unprefix("PROGRAM START \"", s)
s2 <- Library.try_unsuffix("\" ...", s1)
} yield s2
@@ -290,6 +293,8 @@
): Directory = {
val doc_dir = make_directory(dir, doc)
+ progress.echo(program_start("Creating directory"))
+
/* actual sources: with SHA1 digest */
@@ -319,6 +324,8 @@
isabelle_logo.foreach(_.write(doc_dir))
session_graph.write(doc_dir)
+ progress.bash("ls -alR", echo = true, cwd = doc_dir.file).check
+
Directory(doc_dir, doc, root_name, sources)
}
@@ -345,7 +352,7 @@
): String = {
"if [ -f " + root_name_script(ext) + " ]\n" +
"then\n" +
- " " + (if (title.nonEmpty) running_script(title) else "") +
+ " " + (if (title.nonEmpty) program_running_script(title) else "") +
exe + " " + root_name_script() + "\n" +
(if (after.isEmpty) "" else " " + after) +
"fi\n"
@@ -390,7 +397,7 @@
context.prepare_directory(dir, doc, new Latex.Output(context.options))
def use_pdflatex: Boolean = false
- def running_latex: String = running_script(if (use_pdflatex) "pdflatex" else "lualatex")
+ def running_latex: String = program_running_script(if (use_pdflatex) "pdflatex" else "lualatex")
def latex_script(context: Context, directory: Directory): String =
running_latex + (if (use_pdflatex) "$ISABELLE_PDFLATEX" else "$ISABELLE_LUALATEX") +
" " + directory.root_name_script() + "\n"
--- a/src/Pure/Thy/export.scala Wed Feb 01 12:43:39 2023 +0000
+++ b/src/Pure/Thy/export.scala Wed Feb 01 21:29:35 2023 +0100
@@ -447,10 +447,7 @@
for {
name <- theory_context.files0(permissive = true).headOption
file <- get_source_file(name)
- } yield {
- val text0 = file.bytes.text
- if (unicode_symbols) Symbol.decode(text0) else text0
- }
+ } yield Symbol.output(unicode_symbols, file.bytes.text)
}
snapshot_source orElse db_source getOrElse ""
--- a/src/Tools/jEdit/src/document_dockable.scala Wed Feb 01 12:43:39 2023 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala Wed Feb 01 21:29:35 2023 +0100
@@ -105,11 +105,11 @@
/* progress */
- class Log_Progress extends Program_Progress(default_program = "build") {
+ class Log_Progress extends Program_Progress(default_title = "build") {
progress =>
override def detect_program(s: String): Option[String] =
- Document_Build.detect_running_script(s)
+ Document_Build.detect_program_start(s)
private val delay: Delay =
Delay.first(PIDE.session.output_delay) {
@@ -313,12 +313,6 @@
override def clicked(): Unit = pending_process()
}
- private val cancel_button =
- new GUI.Button("Cancel") {
- tooltip = "Cancel build process"
- override def clicked(): Unit = cancel_process()
- }
-
private val view_button =
new GUI.Button("View") {
tooltip = "View document"
@@ -327,7 +321,7 @@
private val controls =
Wrap_Panel(List(document_session, process_indicator.component,
- auto_build_button, build_button, view_button, cancel_button))
+ auto_build_button, build_button, view_button))
add(controls.peer, BorderLayout.NORTH)
@@ -371,8 +365,14 @@
layout(theories_pane) = BorderPanel.Position.Center
}, "Selection and status of document theories")
- private val output_controls =
- Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
+ private val cancel_button =
+ new GUI.Button("Cancel") {
+ tooltip = "Cancel build process"
+ override def clicked(): Unit = cancel_process()
+ }
+
+ private val output_controls = Wrap_Panel(List(cancel_button, zoom))
private val output_page =
new TabbedPane.Page("Output", new BorderPanel {