60 |
60 |
61 /* update */ |
61 /* update */ |
62 |
62 |
63 val path_cartouches = options.bool("update_path_cartouches") |
63 val path_cartouches = options.bool("update_path_cartouches") |
64 |
64 |
65 def update_xml(xml: XML.Body): XML.Body = |
65 def update_xml(lang: Markup.Language.Value, xml: XML.Body): XML.Body = |
66 xml flatMap { |
66 xml flatMap { |
67 case XML.Wrapped_Elem(markup, body1, body2) => |
67 case XML.Wrapped_Elem(markup, body1, body2) => |
68 if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2) |
68 val body = if (markup.name == Markup.UPDATE) body1 else body2 |
69 case XML.Elem(Markup.Language(lang), body) |
69 update_xml(lang, body) |
70 if lang.is_path && path_cartouches => |
70 case XML.Elem(Markup.Language(lang), body) => |
71 Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match { |
71 if (lang.is_path && path_cartouches) { |
72 case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content))) |
72 Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match { |
73 case None => update_xml(body) |
73 case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content))) |
|
74 case None => update_xml(lang, body) |
|
75 } |
74 } |
76 } |
75 case XML.Elem(_, body) => update_xml(body) |
77 else update_xml(lang, body) |
|
78 case XML.Elem(_, body) => update_xml(lang, body) |
76 case t => List(t) |
79 case t => List(t) |
77 } |
80 } |
78 |
81 |
79 var seen_theory = Set.empty[String] |
82 var seen_theory = Set.empty[String] |
80 |
83 |
100 snapshot = theory_snapshot.switch(node_name) |
103 snapshot = theory_snapshot.switch(node_name) |
101 if snapshot.node.source_wellformed |
104 if snapshot.node.source_wellformed |
102 } { |
105 } { |
103 progress.expose_interrupt() |
106 progress.expose_interrupt() |
104 val source1 = |
107 val source1 = |
105 XML.content(update_xml( |
108 XML.content(update_xml(Markup.Language.outer, |
106 snapshot.xml_markup(elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)))) |
109 snapshot.xml_markup(elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE)))) |
107 if (source1 != snapshot.node.source) { |
110 if (source1 != snapshot.node.source) { |
108 val path = Path.explode(node_name.node) |
111 val path = Path.explode(node_name.node) |
109 progress.echo("Updating " + quote(File.standard_path(path))) |
112 progress.echo("Updating " + quote(File.standard_path(path))) |
110 File.write(path, source1) |
113 File.write(path, source1) |