--- 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"
--- 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,
--- 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] =
--- 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)) {