author | wenzelm |
Thu, 12 Aug 2010 15:19:11 +0200 | |
changeset 38363 | af7f41a8a0a8 |
parent 38355 | 8cb265fb12fe |
child 38370 | 8b15d0f98962 |
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 |
{ |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
12 |
/* protocol messages */ |
36682 | 13 |
|
14 |
object Assign { |
|
15 |
def unapply(msg: XML.Tree): Option[List[XML.Tree]] = |
|
16 |
msg match { |
|
38231 | 17 |
case XML.Elem(Markup.Assign, edits) => Some(edits) |
36682 | 18 |
case _ => None |
19 |
} |
|
20 |
} |
|
21 |
||
22 |
object Edit { |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
23 |
def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_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) => |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
26 |
(Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match { |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
27 |
case (Some(i), Some(j)) => Some((i, j)) |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
28 |
case _ => None |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
29 |
} |
36682 | 30 |
case _ => None |
31 |
} |
|
32 |
} |
|
29645 | 33 |
} |
34 |
||
32450 | 35 |
|
32467 | 36 |
trait Isar_Document extends Isabelle_Process |
29645 | 37 |
{ |
32467 | 38 |
import Isar_Document._ |
29553 | 39 |
|
40 |
||
41 |
/* commands */ |
|
42 |
||
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38259
diff
changeset
|
43 |
def define_command(id: Document.Command_ID, text: String): Unit = |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
44 |
input("Isar_Document.define_command", Document.print_id(id), text) |
29553 | 45 |
|
46 |
||
47 |
/* documents */ |
|
48 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
36682
diff
changeset
|
49 |
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
|
50 |
edits: List[Document.Edit[Document.Command_ID]]) |
29553 | 51 |
{ |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38259
diff
changeset
|
52 |
def make_id1(id1: Option[Document.Command_ID]): XML.Body = |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
53 |
XML_Data.make_long(id1 getOrElse Document.NO_ID) |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
54 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38259
diff
changeset
|
55 |
val arg = |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38259
diff
changeset
|
56 |
XML_Data.make_list( |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38259
diff
changeset
|
57 |
XML_Data.make_pair(XML_Data.make_string)( |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38259
diff
changeset
|
58 |
XML_Data.make_option(XML_Data.make_list( |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
59 |
XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits) |
29553 | 60 |
|
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
61 |
input("Isar_Document.edit_document", |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38271
diff
changeset
|
62 |
Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg)) |
29553 | 63 |
} |
64 |
} |