# HG changeset patch
# User wenzelm
# Date 1675283375 -3600
# Node ID dad9960852a268ada5829ba361eb500fe91a47ed
# Parent  052aab920a52e8850bd2a3defac8cd09498c8fd9# Parent  1eb55d6809b3c26de3114779984da8ccc3d92908
merged

diff -r 052aab920a52 -r dad9960852a2 src/HOL/BNF_Cardinal_Order_Relation.thy
--- 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| )"
diff -r 052aab920a52 -r dad9960852a2 src/HOL/Binomial.thy
--- 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>
diff -r 052aab920a52 -r dad9960852a2 src/HOL/GCD.thy
--- 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)"
diff -r 052aab920a52 -r dad9960852a2 src/HOL/HOL.thy
--- 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
diff -r 052aab920a52 -r dad9960852a2 src/HOL/Wellfounded.thy
--- 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"
diff -r 052aab920a52 -r dad9960852a2 src/Pure/Admin/isabelle_cronjob.scala
--- 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" +
diff -r 052aab920a52 -r dad9960852a2 src/Pure/PIDE/headless.scala
--- 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)
         }
diff -r 052aab920a52 -r dad9960852a2 src/Pure/System/progress.scala
--- 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)
     }
   }
diff -r 052aab920a52 -r dad9960852a2 src/Pure/Thy/document_build.scala
--- 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"
diff -r 052aab920a52 -r dad9960852a2 src/Pure/Thy/export.scala
--- 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 ""
diff -r 052aab920a52 -r dad9960852a2 src/Tools/jEdit/src/document_dockable.scala
--- 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 {