1 /* Title: Pure/PIDE/isabelle_document.scala |
|
2 Author: Makarius |
|
3 |
|
4 Protocol message formats for interactive Isar documents. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Isabelle_Document |
|
11 { |
|
12 /* document editing */ |
|
13 |
|
14 object Assign |
|
15 { |
|
16 def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] = |
|
17 try { |
|
18 import XML.Decode._ |
|
19 val body = YXML.parse_body(text) |
|
20 Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body)) |
|
21 } |
|
22 catch { |
|
23 case ERROR(_) => None |
|
24 case _: XML.XML_Atom => None |
|
25 case _: XML.XML_Body => None |
|
26 } |
|
27 } |
|
28 |
|
29 object Removed |
|
30 { |
|
31 def unapply(text: String): Option[List[Document.Version_ID]] = |
|
32 try { |
|
33 import XML.Decode._ |
|
34 Some(list(long)(YXML.parse_body(text))) |
|
35 } |
|
36 catch { |
|
37 case ERROR(_) => None |
|
38 case _: XML.XML_Atom => None |
|
39 case _: XML.XML_Body => None |
|
40 } |
|
41 } |
|
42 |
|
43 |
|
44 /* toplevel transactions */ |
|
45 |
|
46 sealed abstract class Status |
|
47 case object Unprocessed extends Status |
|
48 case class Forked(forks: Int) extends Status |
|
49 case object Finished extends Status |
|
50 case object Failed extends Status |
|
51 |
|
52 def command_status(markup: List[Markup]): Status = |
|
53 { |
|
54 val forks = (0 /: markup) { |
|
55 case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1 |
|
56 case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1 |
|
57 case (i, _) => i |
|
58 } |
|
59 if (forks != 0) Forked(forks) |
|
60 else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed |
|
61 else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished |
|
62 else Unprocessed |
|
63 } |
|
64 |
|
65 sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) |
|
66 { |
|
67 def total: Int = unprocessed + running + finished + failed |
|
68 } |
|
69 |
|
70 def node_status( |
|
71 state: Document.State, version: Document.Version, node: Document.Node): Node_Status = |
|
72 { |
|
73 var unprocessed = 0 |
|
74 var running = 0 |
|
75 var finished = 0 |
|
76 var failed = 0 |
|
77 node.commands.foreach(command => |
|
78 command_status(state.command_state(version, command).status) match { |
|
79 case Unprocessed => unprocessed += 1 |
|
80 case Forked(_) => running += 1 |
|
81 case Finished => finished += 1 |
|
82 case Failed => failed += 1 |
|
83 }) |
|
84 Node_Status(unprocessed, running, finished, failed) |
|
85 } |
|
86 |
|
87 |
|
88 /* result messages */ |
|
89 |
|
90 def clean_message(body: XML.Body): XML.Body = |
|
91 body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map |
|
92 { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t } |
|
93 |
|
94 def message_reports(msg: XML.Tree): List[XML.Elem] = |
|
95 msg match { |
|
96 case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem) |
|
97 case XML.Elem(_, body) => body.flatMap(message_reports) |
|
98 case XML.Text(_) => Nil |
|
99 } |
|
100 |
|
101 |
|
102 /* specific messages */ |
|
103 |
|
104 def is_ready(msg: XML.Tree): Boolean = |
|
105 msg match { |
|
106 case XML.Elem(Markup(Isabelle_Markup.STATUS, _), |
|
107 List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true |
|
108 case _ => false |
|
109 } |
|
110 |
|
111 def is_tracing(msg: XML.Tree): Boolean = |
|
112 msg match { |
|
113 case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true |
|
114 case _ => false |
|
115 } |
|
116 |
|
117 def is_warning(msg: XML.Tree): Boolean = |
|
118 msg match { |
|
119 case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true |
|
120 case _ => false |
|
121 } |
|
122 |
|
123 def is_error(msg: XML.Tree): Boolean = |
|
124 msg match { |
|
125 case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true |
|
126 case _ => false |
|
127 } |
|
128 |
|
129 def is_state(msg: XML.Tree): Boolean = |
|
130 msg match { |
|
131 case XML.Elem(Markup(Isabelle_Markup.WRITELN, _), |
|
132 List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true |
|
133 case _ => false |
|
134 } |
|
135 |
|
136 |
|
137 /* reported positions */ |
|
138 |
|
139 private val include_pos = |
|
140 Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT, |
|
141 Isabelle_Markup.POSITION) |
|
142 |
|
143 def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = |
|
144 { |
|
145 def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = |
|
146 tree match { |
|
147 case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body) |
|
148 if include_pos(name) && id == command.id => |
|
149 val range = command.decode(raw_range).restrict(command.range) |
|
150 body.foldLeft(if (range.is_singularity) set else set + range)(positions) |
|
151 case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions) |
|
152 case _ => set |
|
153 } |
|
154 val set = positions(Set.empty, message) |
|
155 if (set.isEmpty && !is_state(message)) |
|
156 set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) |
|
157 else set |
|
158 } |
|
159 } |
|
160 |
|
161 |
|
162 trait Isabelle_Document extends Isabelle_Process |
|
163 { |
|
164 /* commands */ |
|
165 |
|
166 def define_command(command: Command): Unit = |
|
167 input("Isabelle_Document.define_command", |
|
168 Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source)) |
|
169 |
|
170 |
|
171 /* document versions */ |
|
172 |
|
173 def cancel_execution() |
|
174 { |
|
175 input("Isabelle_Document.cancel_execution") |
|
176 } |
|
177 |
|
178 def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, |
|
179 name: Document.Node.Name, perspective: Command.Perspective) |
|
180 { |
|
181 val ids = |
|
182 { import XML.Encode._ |
|
183 list(long)(perspective.commands.map(_.id)) } |
|
184 |
|
185 input("Isabelle_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), |
|
186 name.node, YXML.string_of_body(ids)) |
|
187 } |
|
188 |
|
189 def update(old_id: Document.Version_ID, new_id: Document.Version_ID, |
|
190 edits: List[Document.Edit_Command]) |
|
191 { |
|
192 val edits_yxml = |
|
193 { import XML.Encode._ |
|
194 def id: T[Command] = (cmd => long(cmd.id)) |
|
195 def encode_edit(dir: String) |
|
196 : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = |
|
197 variant(List( |
|
198 { case Document.Node.Clear() => (Nil, Nil) }, |
|
199 { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
|
200 { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => |
|
201 (Nil, |
|
202 triple(pair(string, string), list(string), list(pair(string, bool)))( |
|
203 (dir, a), b, c)) }, |
|
204 { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, |
|
205 { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) |
|
206 def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => |
|
207 { |
|
208 val (name, edit) = node_edit |
|
209 val dir = Isabelle_System.posix_path(name.dir) |
|
210 pair(string, encode_edit(dir))(name.node, edit) |
|
211 }) |
|
212 YXML.string_of_body(encode(edits)) } |
|
213 input("Isabelle_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml) |
|
214 } |
|
215 |
|
216 def remove_versions(versions: List[Document.Version]) |
|
217 { |
|
218 val versions_yxml = |
|
219 { import XML.Encode._ |
|
220 YXML.string_of_body(list(long)(versions.map(_.id))) } |
|
221 input("Isabelle_Document.remove_versions", versions_yxml) |
|
222 } |
|
223 |
|
224 |
|
225 /* method invocation service */ |
|
226 |
|
227 def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String) |
|
228 { |
|
229 input("Isabelle_Document.invoke_scala", id, tag.toString, res) |
|
230 } |
|
231 } |
|