# HG changeset patch
# User wenzelm
# Date 1546774946 -3600
# Node ID 67ae2e164c0fd2543e575e7e202462e0c46f028b
# Parent  48e9732510705bfd0894e33d1fa9188aa81e2c3f
support for isabelle update -u path_cartouches;

diff -r 48e973251070 -r 67ae2e164c0f etc/options
--- a/etc/options	Sun Jan 06 12:33:45 2019 +0100
+++ b/etc/options	Sun Jan 06 12:42:26 2019 +0100
@@ -288,6 +288,9 @@
 option update_control_cartouches : bool = false
   -- "update antiquotations to use control symbol with cartouche argument"
 
+option update_path_cartouches : bool = false
+  -- "update file-system paths to use cartouches"
+
 
 section "Build Database"
 
diff -r 48e973251070 -r 67ae2e164c0f src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Jan 06 12:33:45 2019 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Jan 06 12:42:26 2019 +0100
@@ -734,6 +734,10 @@
     example, ``\<open>@{term \<doublequote>x + y\<doublequote>}\<close>'' is replaced by
     ``\<open>\<^term>\<open>x + y\<close>\<close>'' (the control symbol is literally \<^verbatim>\<open>\<^term>\<close>.)
 
+    \<^item> @{system_option update_path_cartouches} to update file-system paths to
+    use cartouches: this depends on language markup provided by semantic
+    processing of parsed input.
+
   It is also possible to produce custom updates in Isabelle/ML, by reporting
   \<^ML>\<open>Markup.update\<close> with the precise source position and a replacement
   text. This operation should be made conditional on specific system options,
diff -r 48e973251070 -r 67ae2e164c0f src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sun Jan 06 12:33:45 2019 +0100
+++ b/src/Pure/Isar/token.scala	Sun Jan 06 12:42:26 2019 +0100
@@ -156,6 +156,15 @@
   val newline: Token = explode(Keyword.Keywords.empty, "\n").head
 
 
+  /* embedded */
+
+  def read_embedded(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
+    explode(keywords, inp) match {
+      case List(tok) if tok.is_embedded => Some(tok)
+      case _ => None
+    }
+
+
   /* names */
 
   def read_name(keywords: Keyword.Keywords, inp: CharSequence): Option[Token] =
diff -r 48e973251070 -r 67ae2e164c0f src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sun Jan 06 12:33:45 2019 +0100
+++ b/src/Pure/Tools/update.scala	Sun Jan 06 12:42:26 2019 +0100
@@ -31,10 +31,18 @@
         session_dirs = dirs ::: select_dirs,
         include_sessions = deps.sessions_structure.imports_topological_order)
 
+    val path_cartouches = dump_options.bool("update_path_cartouches")
+
     def update_xml(xml: XML.Body): XML.Body =
       xml flatMap {
         case XML.Wrapped_Elem(markup, body1, body2) =>
           if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
+        case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
+        if path_cartouches =>
+          Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
+            case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
+            case None => update_xml(body)
+          }
         case XML.Elem(_, body) => update_xml(body)
         case t => List(t)
       }
@@ -48,7 +56,7 @@
           for ((node_name, node) <- snapshot.nodes) {
             val xml =
               snapshot.state.markup_to_XML(snapshot.version, node_name,
-                Text.Range.full, Markup.Elements(Markup.UPDATE))
+                Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
 
             val source1 = Symbol.encode(XML.content(update_xml(xml)))
             if (source1 != Symbol.encode(node.source)) {