author | wenzelm |
Fri, 02 Oct 2009 22:15:08 +0200 | |
changeset 32861 | 105f40051387 |
parent 32467 | 4dab52ca1402 |
child 36682 | 3f989067f87d |
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 |
|
29645 | 17 |
} |
18 |
||
32450 | 19 |
|
32467 | 20 |
trait Isar_Document extends Isabelle_Process |
29645 | 21 |
{ |
32467 | 22 |
import Isar_Document._ |
29553 | 23 |
|
24 |
||
25 |
/* commands */ |
|
26 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
27 |
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
|
28 |
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
|
29 |
Isabelle_Syntax.encode_string(text)) |
29553 | 30 |
} |
31 |
||
32 |
||
33 |
/* documents */ |
|
34 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
35 |
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
|
36 |
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
|
37 |
Isabelle_Syntax.encode_string(path)) |
29553 | 38 |
} |
39 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
40 |
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
|
41 |
output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id)) |
29553 | 42 |
} |
43 |
||
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
44 |
def edit_document(old_id: Document_ID, new_id: Document_ID, |
29553 | 45 |
edits: List[(Command_ID, Option[Command_ID])]) |
46 |
{ |
|
47 |
def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder) |
|
48 |
{ |
|
49 |
edit match { |
|
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
50 |
case (id, None) => Isabelle_Syntax.append_string(id, result) |
29553 | 51 |
case (id, Some(id2)) => |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
52 |
Isabelle_Syntax.append_string(id, result) |
29553 | 53 |
result.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
54 |
Isabelle_Syntax.append_string(id2, result) |
29553 | 55 |
} |
56 |
} |
|
57 |
||
58 |
val buf = new StringBuilder(40) |
|
59 |
buf.append("Isar.edit_document ") |
|
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
60 |
Isabelle_Syntax.append_string(old_id, buf) |
29553 | 61 |
buf.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
62 |
Isabelle_Syntax.append_string(new_id, buf) |
29553 | 63 |
buf.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
64 |
Isabelle_Syntax.append_list(append_edit, edits, buf) |
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
65 |
output_sync(buf.toString) |
29553 | 66 |
} |
67 |
} |