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