# HG changeset patch
# User wenzelm
# Date 1621345563 -7200
# Node ID 5a3a2a52648d3e7488bb0e275f9c683ddc88cb38
# Parent  1bbbaae6b5e346344e095372857912a06e9897aa
clarified treatment of Isabelle .sty files;

diff -r 1bbbaae6b5e3 -r 5a3a2a52648d NEWS
--- a/NEWS	Tue May 18 15:17:55 2021 +0200
+++ b/NEWS	Tue May 18 15:46:03 2021 +0200
@@ -56,6 +56,10 @@
 explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
 adjust session ROOT options.
 
+* Isabelle .sty files are automatically generated within the document
+output directory; former "isabelle latex -o sty" has been discontinued.
+Minor INCOMPATIBILITY in document build scripts.
+
 * Improved LaTeX typesetting of \<open>...\<close> using \guilsinglleft ...
 \guilsinglright. INCOMPATIBILITY, need to use \usepackage[T1]{fontenc}
 (which is now also the default in "isabelle mkroot").
diff -r 1bbbaae6b5e3 -r 5a3a2a52648d src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Tue May 18 15:17:55 2021 +0200
+++ b/src/Doc/System/Presentation.thy	Tue May 18 15:46:03 2021 +0200
@@ -188,7 +188,7 @@
 \<open>Usage: isabelle latex [OPTIONS] [FILE]
 
   Options are:
-    -o FORMAT    specify output format: pdf (default), bbl, idx, sty
+    -o FORMAT    specify output format: pdf (default), bbl, idx
 
   Run LaTeX (and related tools) on FILE (default root.tex),
   producing the specified output format.\<close>}
@@ -198,10 +198,6 @@
   (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands
   are determined from the settings environment (@{setting ISABELLE_PDFLATEX}
   etc.).
-
-  The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
-  the distribution. This is useful in special situations where the document
-  sources are to be processed another time by separate tools.
 \<close>
 
 
diff -r 1bbbaae6b5e3 -r 5a3a2a52648d src/Doc/prepare_document
--- a/src/Doc/prepare_document	Tue May 18 15:17:55 2021 +0200
+++ b/src/Doc/prepare_document	Tue May 18 15:46:03 2021 +0200
@@ -4,7 +4,6 @@
 
 FORMAT="$1"
 
-isabelle latex -o sty
 cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" .
 
 isabelle latex -o "$FORMAT"
@@ -13,4 +12,3 @@
 isabelle latex -o "$FORMAT"
 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
 isabelle latex -o "$FORMAT"
-
diff -r 1bbbaae6b5e3 -r 5a3a2a52648d src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue May 18 15:17:55 2021 +0200
+++ b/src/Pure/Thy/document_build.scala	Tue May 18 15:46:03 2021 +0200
@@ -11,6 +11,11 @@
 {
   /* document variants */
 
+  sealed case class Content(path: Path, bytes: Bytes)
+  {
+    def write(dir: Path): Unit = Bytes.write(dir + path, bytes)
+  }
+
   abstract class Document_Name
   {
     def name: String
@@ -37,15 +42,20 @@
     def print_tags: String = tags.mkString(",")
     def print: String = if (tags.isEmpty) name else name + "=" + print_tags
 
-    def latex_sty: String =
-      Library.terminate_lines(
-        tags.map(tag =>
-          tag.toList match {
-            case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
-            case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
-            case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
-            case cs => "\\isakeeptag{" + cs.mkString + "}"
-          }))
+    def isabelletags: Content =
+    {
+      val path = Path.explode("isabelletags.sty")
+      val text =
+        Library.terminate_lines(
+          tags.map(tag =>
+            tag.toList match {
+              case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}"
+              case '-' :: cs => "\\isadroptag{" + cs.mkString + "}"
+              case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
+              case cs => "\\isakeeptag{" + cs.mkString + "}"
+            }))
+      Content(path, Bytes(text))
+    }
   }
 
   sealed case class Document_Input(name: String, sources: SHA1.Digest)
@@ -132,6 +142,10 @@
 
   /* context */
 
+  val isabelle_styles: List[Path] =
+    List("comment.sty", "isabelle.sty", "isabellesym.sty", "pdfsetup.sty", "railsetup.sty").
+      map(name => Path.explode("~~/lib/texinputs") + Path.basic(name))
+
   def context(
     session: String,
     deps: Sessions.Deps,
@@ -229,8 +243,9 @@
 
       /* sources */
 
-      Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
-      File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty)
+      isabelle_styles.foreach(Isabelle_System.copy_file(_, doc_dir))
+      doc.isabelletags.write(doc_dir)
+
       for ((base_dir, src) <- info.document_files) {
         Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir)
       }
@@ -263,11 +278,6 @@
       yield old_doc
   }
 
-  sealed case class Content(path: Path, bytes: Bytes)
-  {
-    def write(dir: Path): Unit = Bytes.write(dir + path, bytes)
-  }
-
   sealed case class Directory(
     doc_dir: Path,
     doc: Document_Variant,