author | wenzelm |
Sat, 07 Aug 2010 22:09:52 +0200 | |
changeset 38230 | ed147003de4b |
parent 38150 | 67fc24df3721 |
child 38231 | 968844caaff9 |
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 |
{ |
36682 | 12 |
/* reports */ |
13 |
||
14 |
object Assign { |
|
15 |
def unapply(msg: XML.Tree): Option[List[XML.Tree]] = |
|
16 |
msg match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
38150
diff
changeset
|
17 |
case XML.Elem(Markup(Markup.ASSIGN, Nil), edits) => Some(edits) |
36682 | 18 |
case _ => None |
19 |
} |
|
20 |
} |
|
21 |
||
22 |
object Edit { |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
23 |
def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] = |
36682 | 24 |
msg match { |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
38150
diff
changeset
|
25 |
case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) => |
36682 | 26 |
Some(cmd_id, state_id) |
27 |
case _ => None |
|
28 |
} |
|
29 |
} |
|
29645 | 30 |
} |
31 |
||
32450 | 32 |
|
32467 | 33 |
trait Isar_Document extends Isabelle_Process |
29645 | 34 |
{ |
32467 | 35 |
import Isar_Document._ |
29553 | 36 |
|
37 |
||
38 |
/* commands */ |
|
39 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
40 |
def define_command(id: Document.Command_ID, text: String) { |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
41 |
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
|
42 |
Isabelle_Syntax.encode_string(text)) |
29553 | 43 |
} |
44 |
||
45 |
||
46 |
/* documents */ |
|
47 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
48 |
def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID, |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
49 |
edits: List[Document.Edit[Document.Command_ID]]) |
29553 | 50 |
{ |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
51 |
def append_edit( |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
52 |
edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder) |
29553 | 53 |
{ |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
54 |
Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
55 |
edit._2 match { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
56 |
case None => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
57 |
case Some(id2) => |
29553 | 58 |
result.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
59 |
Isabelle_Syntax.append_string(id2, result) |
29553 | 60 |
} |
61 |
} |
|
62 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
63 |
def append_node_edit( |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
64 |
edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]), |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
65 |
result: StringBuilder) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
66 |
{ |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
67 |
Isabelle_Syntax.append_string(edit._1, result) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
68 |
edit._2 match { |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
69 |
case None => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
70 |
case Some(eds) => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
71 |
result.append(" ") |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
72 |
Isabelle_Syntax.append_list(append_edit, eds, result) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
73 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
74 |
} |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
75 |
|
29553 | 76 |
val buf = new StringBuilder(40) |
77 |
buf.append("Isar.edit_document ") |
|
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
78 |
Isabelle_Syntax.append_string(old_id, buf) |
29553 | 79 |
buf.append(" ") |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
80 |
Isabelle_Syntax.append_string(new_id, buf) |
29553 | 81 |
buf.append(" ") |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
82 |
Isabelle_Syntax.append_list(append_node_edit, edits, buf) |
29644
fbbd0197155c
turned IsarDocument into trait for IsabelleProcess;
wenzelm
parents:
29553
diff
changeset
|
83 |
output_sync(buf.toString) |
29553 | 84 |
} |
85 |
} |