1 /* Title: Pure/System/isar_document.scala |
|
2 Author: Makarius |
|
3 |
|
4 Protocol commands for interactive Isar documents. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Isar_Document |
|
11 { |
|
12 /* protocol messages */ |
|
13 |
|
14 object Assign { |
|
15 def unapply(msg: XML.Tree) |
|
16 : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] = |
|
17 msg match { |
|
18 case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) => |
|
19 val id_edits = edits.map(Edit.unapply) |
|
20 if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get))) |
|
21 else None |
|
22 case _ => None |
|
23 } |
|
24 } |
|
25 |
|
26 object Edit { |
|
27 def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = |
|
28 msg match { |
|
29 case XML.Elem( |
|
30 Markup(Markup.EDIT, |
|
31 List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j)) |
|
32 case _ => None |
|
33 } |
|
34 } |
|
35 } |
|
36 |
|
37 |
|
38 trait Isar_Document extends Isabelle_Process |
|
39 { |
|
40 import Isar_Document._ |
|
41 |
|
42 |
|
43 /* commands */ |
|
44 |
|
45 def define_command(id: Document.Command_ID, text: String): Unit = |
|
46 input("Isar_Document.define_command", Document.ID(id), text) |
|
47 |
|
48 |
|
49 /* document versions */ |
|
50 |
|
51 def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, |
|
52 edits: List[Document.Edit[Document.Command_ID]]) |
|
53 { |
|
54 val arg = |
|
55 XML_Data.make_list( |
|
56 XML_Data.make_pair(XML_Data.make_string)( |
|
57 XML_Data.make_option(XML_Data.make_list( |
|
58 XML_Data.make_pair( |
|
59 XML_Data.make_option(XML_Data.make_long))( |
|
60 XML_Data.make_option(XML_Data.make_long))))))(edits) |
|
61 |
|
62 input("Isar_Document.edit_version", |
|
63 Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) |
|
64 } |
|
65 } |
|