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