29 val resources = |
29 val resources = |
30 Headless.Resources.make(dump_options, logic, progress = progress, log = log, |
30 Headless.Resources.make(dump_options, logic, progress = progress, log = log, |
31 session_dirs = dirs ::: select_dirs, |
31 session_dirs = dirs ::: select_dirs, |
32 include_sessions = deps.sessions_structure.imports_topological_order) |
32 include_sessions = deps.sessions_structure.imports_topological_order) |
33 |
33 |
|
34 val path_cartouches = dump_options.bool("update_path_cartouches") |
|
35 |
34 def update_xml(xml: XML.Body): XML.Body = |
36 def update_xml(xml: XML.Body): XML.Body = |
35 xml flatMap { |
37 xml flatMap { |
36 case XML.Wrapped_Elem(markup, body1, body2) => |
38 case XML.Wrapped_Elem(markup, body1, body2) => |
37 if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2) |
39 if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2) |
|
40 case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body) |
|
41 if path_cartouches => |
|
42 Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match { |
|
43 case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content))) |
|
44 case None => update_xml(body) |
|
45 } |
38 case XML.Elem(_, body) => update_xml(body) |
46 case XML.Elem(_, body) => update_xml(body) |
39 case t => List(t) |
47 case t => List(t) |
40 } |
48 } |
41 |
49 |
42 Dump.session(deps, resources, progress = progress, |
50 Dump.session(deps, resources, progress = progress, |
46 progress.echo("Processing theory " + snapshot.node_name + " ...") |
54 progress.echo("Processing theory " + snapshot.node_name + " ...") |
47 |
55 |
48 for ((node_name, node) <- snapshot.nodes) { |
56 for ((node_name, node) <- snapshot.nodes) { |
49 val xml = |
57 val xml = |
50 snapshot.state.markup_to_XML(snapshot.version, node_name, |
58 snapshot.state.markup_to_XML(snapshot.version, node_name, |
51 Text.Range.full, Markup.Elements(Markup.UPDATE)) |
59 Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)) |
52 |
60 |
53 val source1 = Symbol.encode(XML.content(update_xml(xml))) |
61 val source1 = Symbol.encode(XML.content(update_xml(xml))) |
54 if (source1 != Symbol.encode(node.source)) { |
62 if (source1 != Symbol.encode(node.source)) { |
55 progress.echo("Updating " + node_name.path) |
63 progress.echo("Updating " + node_name.path) |
56 File.write(node_name.path, source1) |
64 File.write(node_name.path, source1) |