# HG changeset patch
# User wenzelm
# Date 1660312912 -7200
# Node ID a2b2e8964e1aa0164e7f4adc6808a4de0dd999b9
# Parent  6eb8d6cdb6864ea05d3f065a2eff4fa9a95de92a
tuned signature;

diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/General/file.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -301,11 +301,9 @@
 
   /* content */
 
-  object Content {
-    def apply(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
-    def apply(path: Path, content: String): Content_String = new Content_String(path, content)
-    def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
-  }
+  def content(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
+  def content(path: Path, content: String): Content_String = new Content_String(path, content)
+  def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
 
   trait Content {
     def path: Path
diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/General/mercurial.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -323,10 +323,10 @@
 
         Rsync.init(context0, target,
           contents =
-            File.Content(Hg_Sync.PATH_ID, id_content) ::
-            File.Content(Hg_Sync.PATH_LOG, log_content) ::
-            File.Content(Hg_Sync.PATH_DIFF, diff_content) ::
-            File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents)
+            File.content(Hg_Sync.PATH_ID, id_content) ::
+            File.content(Hg_Sync.PATH_LOG, log_content) ::
+            File.content(Hg_Sync.PATH_DIFF, diff_content) ::
+            File.content(Hg_Sync.PATH_STAT, stat_content) :: contents)
 
         val (exclude, source) =
           if (rev.isEmpty) {
diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/Thy/document_build.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -173,13 +173,13 @@
         val path = Path.basic(tex_name(name))
         val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
         val content = YXML.parse_body(entry.text)
-        File.Content(path, content)
+        File.content(path, content)
       }
 
     lazy val session_graph: File.Content = {
       val path = Presentation.session_graph_path
       val content = graphview.Graph_File.make_pdf(options, base.session_graph_display)
-      File.Content(path, content)
+      File.content(path, content)
     }
 
     lazy val session_tex: File.Content = {
@@ -187,7 +187,7 @@
       val content =
         Library.terminate_lines(
           base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}"))
-      File.Content(path, content)
+      File.content(path, content)
     }
 
     lazy val isabelle_logo: Option[File.Content] = {
@@ -196,7 +196,7 @@
           Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
           val path = Path.basic("isabelle_logo.pdf")
           val content = Bytes.read(tmp_path)
-          File.Content(path, content)
+          File.content(path, content)
         })
     }
 
diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -420,7 +420,7 @@
         entry_name <- entry_names(session = session).iterator
         if matcher(entry_name)
         entry <- get(entry_name.theory, entry_name.name).iterator
-      } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList
+      } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
   }
 
   override def toString: String =
diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/Thy/latex.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -133,7 +133,7 @@
       val tags =
         (for ((name, op) <- map.iterator)
           yield "\\isa" + op + "tag{" + name + "}").toList
-      File.Content(path, comment + """
+      File.content(path, comment + """
 
 \newcommand{\isakeeptag}[1]%
 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Pure/Tools/sync.scala
--- a/src/Pure/Tools/sync.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/Tools/sync.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -59,7 +59,7 @@
     context.progress.echo_if(verbose, "\n* Isabelle repository:")
     val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
     sync(hg, target, rev,
-      contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
+      contents = List(File.content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
       filter = filter_heaps ::: List("protect /AFP"))
 
     for (hg <- afp_hg) {
diff -r 6eb8d6cdb686 -r a2b2e8964e1a src/Tools/VSCode/src/build_vscodium.scala
--- a/src/Tools/VSCode/src/build_vscodium.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscodium.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -37,7 +37,7 @@
             "abbrevs" -> entry.abbrevs) ++
           JSON.optional("code", entry.code))
 
-    File.Content(Path.explode("symbols.json"), symbols_js)
+    File.content(Path.explode("symbols.json"), symbols_js)
   }
 
   def make_isabelle_encoding(header: String): File.Content = {
@@ -51,7 +51,7 @@
     val body =
       File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path)
         .replace("[/*symbols*/]", symbols_js)
-    File.Content(path, header + "\n" + body)
+    File.content(path, header + "\n" + body)
   }