# 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, ``\@{term \x + y\}\'' is replaced by ``\\<^term>\x + y\\'' (the control symbol is literally \<^verbatim>\\<^term>\.) + \<^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>\Markup.update\ 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)) {