equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
|
10 import scala.util.matching.Regex |
|
11 |
|
12 |
10 object Update_Cartouches |
13 object Update_Cartouches |
11 { |
14 { |
12 /* update cartouches */ |
15 /* update cartouches */ |
13 |
16 |
14 private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r |
17 private val Verbatim_Body = """(?s)[ \t]*(.*?)[ \t]*""".r |
15 |
18 |
16 val Text_Antiq = """(?s)@\{\s*text\b\s*(.+)\}""".r |
19 val Text_Antiq: Regex = """(?s)@\{\s*text\b\s*(.+)\}""".r |
17 |
20 |
18 def update_text(content: String): String = |
21 def update_text(content: String): String = |
19 { |
22 { |
20 (try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match { |
23 (try { Some(Antiquote.read(content)) } catch { case ERROR(_) => None }) match { |
21 case Some(ants) => |
24 case Some(ants) => |