author | wenzelm |
Sat, 24 Jul 2010 21:22:21 +0200 | |
changeset 37950 | bc285d91041e |
parent 36682 | 3f989067f87d |
child 38150 | 67fc24df3721 |
permissions | -rw-r--r-- |
29553 | 1 |
/* Title: Pure/Isar/isar_document.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Interactive Isar documents. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
32450 | 9 |
|
32467 | 10 |
object Isar_Document |
32450 | 11 |
{ |
29553 | 12 |
/* unique identifiers */ |
13 |
||
14 |
type State_ID = String |
|
15 |
type Command_ID = String |
|
16 |
type Document_ID = String |
|
36682 | 17 |
|
18 |
||
19 |
/* reports */ |
|
20 |
||
21 |
object Assign { |
|
22 |
def unapply(msg: XML.Tree): Option[List[XML.Tree]] = |
|
23 |
msg match { |
|
24 |
case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits) |
|
25 |
case _ => None |
|
26 |
} |
|
27 |
} |
|
28 |
||
29 |
object Edit { |
|
30 |
def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] = |
|
31 |
msg match { |
|
32 |
case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) => |
|
33 |
Some(cmd_id, state_id) |
|
34 |
case _ => None |
|
35 |
} |
|
36 |
} |
|
29645 | 37 |
} |
38 |
||
32450 | 39 |
|
32467 | 40 |
trait Isar_Document extends Isabelle_Process |
29645 | 41 |
{ |
32467 | 42 |
import Isar_Document._ |
29553 | 43 |
|
44 |
||
45 |
/* commands */ |
|
46 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
47 |
def define_command(id: Command_ID, text: String) { |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
48 |
output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " + |
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
49 |
Isabelle_Syntax.encode_string(text)) |
29553 | 50 |
} |
51 |
||
52 |
||
53 |
/* documents */ |
|
54 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
55 |
def begin_document(id: Document_ID, path: String) { |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
56 |
output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " + |
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
57 |
Isabelle_Syntax.encode_string(path)) |
29553 | 58 |
} |
59 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
60 |
def end_document(id: Document_ID) { |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
61 |
output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id)) |
29553 | 62 |
} |
63 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
64 |
def edit_document(old_id: Document_ID, new_id: Document_ID, |
29553 | 65 |
edits: List[(Command_ID, Option[Command_ID])]) |
66 |
{ |
|
67 |
def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder) |
|
68 |
{ |
|
69 |
edit match { |
|
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
70 |
case (id, None) => Isabelle_Syntax.append_string(id, result) |
29553 | 71 |
case (id, Some(id2)) => |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
72 |
Isabelle_Syntax.append_string(id, result) |
29553 | 73 |
result.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
74 |
Isabelle_Syntax.append_string(id2, result) |
29553 | 75 |
} |
76 |
} |
|
77 |
||
78 |
val buf = new StringBuilder(40) |
|
79 |
buf.append("Isar.edit_document ") |
|
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
80 |
Isabelle_Syntax.append_string(old_id, buf) |
29553 | 81 |
buf.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
82 |
Isabelle_Syntax.append_string(new_id, buf) |
29553 | 83 |
buf.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
84 |
Isabelle_Syntax.append_list(append_edit, edits, buf) |
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
85 |
output_sync(buf.toString) |
29553 | 86 |
} |
87 |
} |