author | wenzelm |
Thu, 08 Nov 2018 22:02:07 +0100 | |
changeset 69271 | 4cb70e7e36b9 |
parent 68994 | d961e11e0e87 |
child 71601 | 97ccf48c2f0c |
permissions | -rw-r--r-- |
58610 | 1 |
/* Title: Pure/Tools/update_cartouches.scala |
2 |
Author: Makarius |
|
3 |
||
61579 | 4 |
Update theory syntax to use cartouches etc. |
58610 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Update_Cartouches |
|
11 |
{ |
|
12 |
/* update cartouches */ |
|
13 |
||
14 |
private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r |
|
15 |
||
61492 | 16 |
val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r |
17 |
||
18 |
def update_text(content: String): String = |
|
19 |
{ |
|
20 |
(try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match { |
|
21 |
case Some(ants) => |
|
22 |
val ants1: List[Antiquote.Antiquote] = |
|
23 |
ants.map(ant => |
|
24 |
ant match { |
|
25 |
case Antiquote.Antiq(Text_Antiq(body)) => |
|
26 |
Token.explode(Keyword.Keywords.empty, body).filterNot(_.is_space) match { |
|
67131 | 27 |
case List(tok) => Antiquote.Control(Symbol.cartouche(tok.content)) |
61492 | 28 |
case _ => ant |
29 |
} |
|
30 |
case _ => ant |
|
31 |
}) |
|
32 |
if (ants == ants1) content else ants1.map(_.source).mkString |
|
33 |
case None => content |
|
34 |
} |
|
35 |
} |
|
36 |
||
67433
e0c0c1f0e3e7
more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
wenzelm
parents:
67131
diff
changeset
|
37 |
def update_cartouches(replace_text: Boolean, path: Path) |
58610 | 38 |
{ |
39 |
val text0 = File.read(path) |
|
61492 | 40 |
|
67433
e0c0c1f0e3e7
more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
wenzelm
parents:
67131
diff
changeset
|
41 |
// outer syntax cartouches |
58610 | 42 |
val text1 = |
59083 | 43 |
(for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) |
58610 | 44 |
yield { |
67131 | 45 |
if (tok.kind == Token.Kind.ALT_STRING) Symbol.cartouche(tok.content) |
58610 | 46 |
else if (tok.kind == Token.Kind.VERBATIM) { |
47 |
tok.content match { |
|
67131 | 48 |
case Verbatim_Body(s) => Symbol.cartouche(s) |
58610 | 49 |
case s => tok.source |
50 |
} |
|
51 |
} |
|
52 |
else tok.source |
|
53 |
} |
|
54 |
).mkString |
|
55 |
||
61492 | 56 |
// cartouches within presumed text tokens |
57 |
val text2 = |
|
58 |
if (replace_text) { |
|
59 |
(for (tok <- Token.explode(Keyword.Keywords.empty, text1).iterator) |
|
60 |
yield { |
|
61 |
if (tok.kind == Token.Kind.STRING || tok.kind == Token.Kind.CARTOUCHE) { |
|
62 |
val content = tok.content |
|
63 |
val content1 = update_text(content) |
|
64 |
||
65 |
if (content == content1) tok.source |
|
66 |
else if (tok.kind == Token.Kind.STRING) Outer_Syntax.quote_string(content1) |
|
67131 | 67 |
else Symbol.cartouche(content1) |
61492 | 68 |
} |
69 |
else tok.source |
|
70 |
}).mkString |
|
71 |
} |
|
72 |
else text1 |
|
73 |
||
74 |
if (text0 != text2) { |
|
58610 | 75 |
Output.writeln("changing " + path) |
61492 | 76 |
File.write_backup2(path, text2) |
58610 | 77 |
} |
78 |
} |
|
79 |
||
80 |
||
62836 | 81 |
/* Isabelle tool wrapper */ |
58610 | 82 |
|
62836 | 83 |
val isabelle_tool = |
84 |
Isabelle_Tool("update_cartouches", "update theory syntax to use cartouches", args => |
|
85 |
{ |
|
62445 | 86 |
var replace_text = false |
87 |
||
62454 | 88 |
val getopts = Getopts(""" |
62445 | 89 |
Usage: isabelle update_cartouches [FILES|DIRS...] |
90 |
||
91 |
Options are: |
|
92 |
-t replace @{text} antiquotations within text tokens |
|
93 |
||
69271
4cb70e7e36b9
update ROOT files as well: treated like .thy in Isabelle/jEdit;
wenzelm
parents:
68994
diff
changeset
|
94 |
Recursively find .thy or ROOT files and update theory syntax to use |
4cb70e7e36b9
update ROOT files as well: treated like .thy in Isabelle/jEdit;
wenzelm
parents:
68994
diff
changeset
|
95 |
cartouches instead of old-style {* verbatim *} or `alt_string` tokens. |
62445 | 96 |
|
97 |
Old versions of files are preserved by appending "~~". |
|
98 |
""", |
|
99 |
"t" -> (_ => replace_text = true)) |
|
100 |
||
101 |
val specs = getopts(args) |
|
102 |
if (specs.isEmpty) getopts.usage() |
|
103 |
||
104 |
for { |
|
105 |
spec <- specs |
|
69271
4cb70e7e36b9
update ROOT files as well: treated like .thy in Isabelle/jEdit;
wenzelm
parents:
68994
diff
changeset
|
106 |
file <- File.find_files(Path.explode(spec).file, |
4cb70e7e36b9
update ROOT files as well: treated like .thy in Isabelle/jEdit;
wenzelm
parents:
68994
diff
changeset
|
107 |
file => file.getName.endsWith(".thy") || file.getName == "ROOT") |
68994 | 108 |
} update_cartouches(replace_text, File.path(file)) |
62836 | 109 |
}) |
58610 | 110 |
} |