author | wenzelm |
Fri, 18 Dec 2020 23:19:07 +0100 | |
changeset 72946 | 9329abcdd651 |
parent 72878 | 80465b791f95 |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
1 |
/* Title: Pure/PIDE/protocol.scala |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
4 |
Protocol message formats for interactive proof documents. |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
8 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
9 |
|
45709
87017fcbad83
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents:
45672
diff
changeset
|
10 |
object Protocol |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
11 |
{ |
71630
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
12 |
/* markers for inlined messages */ |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
13 |
|
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
14 |
val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
15 |
val Meta_Info_Marker = Protocol_Message.Marker("meta_info") |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
16 |
val Command_Timing_Marker = Protocol_Message.Marker("command_timing") |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
17 |
val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing") |
72012 | 18 |
val Session_Timing_Marker = Protocol_Message.Marker("session_timing") |
71630
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
19 |
val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics") |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
20 |
val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics") |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
21 |
val Error_Message_Marker = Protocol_Message.Marker("error_message") |
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
22 |
|
50425e4c3910
clarified modules: global quasi-scope for markers;
wenzelm
parents:
71624
diff
changeset
|
23 |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
24 |
/* batch build */ |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
25 |
|
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
26 |
object Loading_Theory |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
27 |
{ |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
28 |
def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] = |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
29 |
(props, props, props) match { |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
30 |
case (Markup.Name(name), Position.File(file), Position.Id(id)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
31 |
if Path.is_wellformed(file) => |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
32 |
val master_dir = Path.explode(file).dir.implode |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
33 |
Some((Document.Node.Name(file, master_dir, name), id)) |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
34 |
case _ => None |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
35 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
36 |
} |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
37 |
|
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
38 |
|
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
39 |
/* document editing */ |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
40 |
|
70665
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
41 |
object Commands_Accepted |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
42 |
{ |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
43 |
def unapply(text: String): Option[List[Document_ID.Command]] = |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
44 |
try { Some(space_explode(',', text).map(Value.Long.parse)) } |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
45 |
catch { case ERROR(_) => None } |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
46 |
|
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
47 |
val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED))) |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
48 |
} |
94442fce40a5
prefer commands_accepted: fewer protocol messages;
wenzelm
parents:
70664
diff
changeset
|
49 |
|
52563 | 50 |
object Assign_Update |
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44474
diff
changeset
|
51 |
{ |
70284
3e17c3a5fd39
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents:
69849
diff
changeset
|
52 |
def unapply(text: String) |
3e17c3a5fd39
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents:
69849
diff
changeset
|
53 |
: Option[(Document_ID.Version, List[String], Document.Assign_Update)] = |
3e17c3a5fd39
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents:
69849
diff
changeset
|
54 |
{ |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
55 |
try { |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
56 |
import XML.Decode._ |
69846 | 57 |
def decode_upd(body: XML.Body): (Long, List[Long]) = |
58 |
space_explode(',', string(body)).map(Value.Long.parse) match { |
|
59 |
case a :: bs => (a, bs) |
|
60 |
case _ => throw new XML.XML_Body(body) |
|
61 |
} |
|
71601 | 62 |
Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text))) |
44661
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
63 |
} |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
64 |
catch { |
383c9d758a56
raw message function "assign_execs" avoids full overhead of decoding and caching message body;
wenzelm
parents:
44644
diff
changeset
|
65 |
case ERROR(_) => None |
51987 | 66 |
case _: XML.Error => None |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
67 |
} |
70284
3e17c3a5fd39
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm
parents:
69849
diff
changeset
|
68 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
69 |
} |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
70 |
|
44676 | 71 |
object Removed |
72 |
{ |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
73 |
def unapply(text: String): Option[List[Document_ID.Version]] = |
44676 | 74 |
try { |
75 |
import XML.Decode._ |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
76 |
Some(list(long)(Symbol.decode_yxml(text))) |
44676 | 77 |
} |
78 |
catch { |
|
79 |
case ERROR(_) => None |
|
51987 | 80 |
case _: XML.Error => None |
44676 | 81 |
} |
82 |
} |
|
83 |
||
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
84 |
|
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
85 |
/* command timing */ |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
86 |
|
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
87 |
object Command_Timing |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
88 |
{ |
71673 | 89 |
def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] = |
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
90 |
props match { |
71673 | 91 |
case Markup.Command_Timing(args) => |
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
92 |
(args, args) match { |
71673 | 93 |
case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing)) |
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
94 |
case _ => None |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
95 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
96 |
case _ => None |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
97 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
98 |
} |
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
99 |
|
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51533
diff
changeset
|
100 |
|
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
101 |
/* theory timing */ |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
102 |
|
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
103 |
object Theory_Timing |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
104 |
{ |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
105 |
def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
106 |
props match { |
71673 | 107 |
case Markup.Theory_Timing(args) => |
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
108 |
(args, args) match { |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
109 |
case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
110 |
case _ => None |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
111 |
} |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
112 |
case _ => None |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
113 |
} |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
114 |
} |
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
115 |
|
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66717
diff
changeset
|
116 |
|
39441
4110cc1b8f9f
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
wenzelm
parents:
39439
diff
changeset
|
117 |
/* result messages */ |
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39181
diff
changeset
|
118 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
119 |
def is_result(msg: XML.Tree): Boolean = |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
120 |
msg match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
121 |
case XML.Elem(Markup(Markup.RESULT, _), _) => true |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
122 |
case _ => false |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
123 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
124 |
|
50157 | 125 |
def is_tracing(msg: XML.Tree): Boolean = |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
126 |
msg match { |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
127 |
case XML.Elem(Markup(Markup.TRACING, _), _) => true |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
128 |
case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true |
39622
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
129 |
case _ => false |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
130 |
} |
53365ba766ac
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
wenzelm
parents:
39511
diff
changeset
|
131 |
|
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
132 |
def is_state(msg: XML.Tree): Boolean = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
133 |
msg match { |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
134 |
case XML.Elem(Markup(Markup.STATE, _), _) => true |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
135 |
case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
136 |
case _ => false |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
137 |
} |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
138 |
|
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
139 |
def is_information(msg: XML.Tree): Boolean = |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
140 |
msg match { |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
141 |
case XML.Elem(Markup(Markup.INFORMATION, _), _) => true |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59085
diff
changeset
|
142 |
case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
143 |
case _ => false |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
144 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
145 |
|
67923
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
146 |
def is_writeln(msg: XML.Tree): Boolean = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
147 |
msg match { |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
148 |
case XML.Elem(Markup(Markup.WRITELN, _), _) => true |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
149 |
case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
150 |
case _ => false |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
151 |
} |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
152 |
|
39511 | 153 |
def is_warning(msg: XML.Tree): Boolean = |
154 |
msg match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
155 |
case XML.Elem(Markup(Markup.WARNING, _), _) => true |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
156 |
case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true |
39511 | 157 |
case _ => false |
158 |
} |
|
159 |
||
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
160 |
def is_legacy(msg: XML.Tree): Boolean = |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
161 |
msg match { |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
162 |
case XML.Elem(Markup(Markup.LEGACY, _), _) => true |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
163 |
case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
164 |
case _ => false |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
165 |
} |
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59184
diff
changeset
|
166 |
|
39511 | 167 |
def is_error(msg: XML.Tree): Boolean = |
168 |
msg match { |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
169 |
case XML.Elem(Markup(Markup.ERROR, _), _) => true |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50157
diff
changeset
|
170 |
case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true |
39511 | 171 |
case _ => false |
172 |
} |
|
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38581
diff
changeset
|
173 |
|
56495 | 174 |
def is_inlined(msg: XML.Tree): Boolean = |
175 |
!(is_result(msg) || is_tracing(msg) || is_state(msg)) |
|
176 |
||
67923
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
177 |
def is_exported(msg: XML.Tree): Boolean = |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
178 |
is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) |
3e072441c96a
clarified exported messages, e.g. suppress "information", "tracing";
wenzelm
parents:
67915
diff
changeset
|
179 |
|
72874 | 180 |
def message_text(elem: XML.Elem, |
72875 | 181 |
heading: Boolean = false, |
182 |
pos: Position.T = Position.none, |
|
71649 | 183 |
margin: Double = Pretty.default_margin, |
184 |
breakgain: Double = Pretty.default_breakgain, |
|
185 |
metric: Pretty.Metric = Pretty.Default_Metric): String = |
|
71165 | 186 |
{ |
72875 | 187 |
val text1 = |
188 |
if (heading) { |
|
189 |
val h = |
|
190 |
if (is_warning(elem) || is_legacy(elem)) "Warning" |
|
191 |
else if (is_error(elem)) "Error" |
|
192 |
else if (is_information(elem)) "Information" |
|
193 |
else if (is_tracing(elem)) "Tracing" |
|
72878 | 194 |
else if (is_state(elem)) "State" |
72875 | 195 |
else "Output" |
72877 | 196 |
"\n" + h + Position.here(pos) + ":\n" |
72875 | 197 |
} |
198 |
else "" |
|
72877 | 199 |
|
200 |
val body = |
|
72874 | 201 |
Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)), |
71649 | 202 |
margin = margin, breakgain = breakgain, metric = metric) |
203 |
||
72877 | 204 |
val text2 = |
205 |
if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body) |
|
206 |
else if (is_error(elem)) Output.error_prefix(body) |
|
207 |
else body |
|
208 |
||
209 |
text1 + text2 |
|
71165 | 210 |
} |
211 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
212 |
|
71624 | 213 |
/* export */ |
214 |
||
215 |
object Export |
|
216 |
{ |
|
217 |
sealed case class Args( |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
218 |
id: Option[String] = None, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
219 |
serial: Long = 0L, |
71624 | 220 |
theory_name: String, |
221 |
name: String, |
|
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
222 |
executable: Boolean = false, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
223 |
compress: Boolean = true, |
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72637
diff
changeset
|
224 |
strict: Boolean = true) |
71624 | 225 |
{ |
226 |
def compound_name: String = isabelle.Export.compound_name(theory_name, name) |
|
227 |
} |
|
228 |
||
229 |
def unapply(props: Properties.T): Option[Args] = |
|
230 |
props match { |
|
231 |
case |
|
232 |
List( |
|
233 |
(Markup.FUNCTION, Markup.EXPORT), |
|
234 |
(Markup.ID, id), |
|
235 |
(Markup.SERIAL, Value.Long(serial)), |
|
236 |
(Markup.THEORY_NAME, theory_name), |
|
237 |
(Markup.NAME, name), |
|
238 |
(Markup.EXECUTABLE, Value.Boolean(executable)), |
|
239 |
(Markup.COMPRESS, Value.Boolean(compress)), |
|
240 |
(Markup.STRICT, Value.Boolean(strict))) => |
|
241 |
Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict)) |
|
242 |
case _ => None |
|
243 |
} |
|
244 |
} |
|
245 |
||
246 |
||
60882 | 247 |
/* breakpoints */ |
248 |
||
249 |
object ML_Breakpoint |
|
250 |
{ |
|
251 |
def unapply(tree: XML.Tree): Option[Long] = |
|
252 |
tree match { |
|
253 |
case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) |
|
254 |
case _ => None |
|
255 |
} |
|
256 |
} |
|
257 |
||
258 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
259 |
/* dialogs */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
260 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
261 |
object Dialog_Args |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
262 |
{ |
52531 | 263 |
def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
264 |
(props, props, props) match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
265 |
case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
266 |
Some((id, serial, result)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
267 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
268 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
269 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
270 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
271 |
object Dialog |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
272 |
{ |
52531 | 273 |
def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
274 |
tree match { |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
275 |
case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
276 |
Some((id, serial, result)) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
277 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
278 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
279 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
280 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
281 |
object Dialog_Result |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
282 |
{ |
52531 | 283 |
def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
284 |
{ |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
285 |
val props = Position.Id(id) ::: Markup.Serial(serial) |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
286 |
XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) |
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
287 |
} |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
288 |
|
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
289 |
def unapply(tree: XML.Tree): Option[String] = |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
290 |
tree match { |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
291 |
case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
292 |
case _ => None |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
293 |
} |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
294 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
295 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
296 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
297 |
|
57916 | 298 |
trait Protocol |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
299 |
{ |
57916 | 300 |
/* protocol commands */ |
301 |
||
70661 | 302 |
def protocol_command_raw(name: String, args: List[Bytes]): Unit |
303 |
def protocol_command_args(name: String, args: List[String]) |
|
57916 | 304 |
def protocol_command(name: String, args: String*): Unit |
305 |
||
306 |
||
56387 | 307 |
/* options */ |
308 |
||
309 |
def options(opts: Options): Unit = |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
310 |
protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) |
56387 | 311 |
|
312 |
||
72637 | 313 |
/* resources */ |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67471
diff
changeset
|
314 |
|
72637 | 315 |
def init_session(resources: Resources): Unit = |
316 |
protocol_command("Prover.init_session", resources.init_session_yxml) |
|
65470 | 317 |
|
318 |
||
56387 | 319 |
/* interned items */ |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
320 |
|
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56306
diff
changeset
|
321 |
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = |
70661 | 322 |
protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes)) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
323 |
|
72946 | 324 |
private def encode_command(resources: Resources, command: Command) |
325 |
: (String, String, String, String, String, List[String]) = |
|
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
326 |
{ |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
327 |
import XML.Encode._ |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
328 |
|
72946 | 329 |
val parents = command.theory_parents(resources).map(name => File.standard_url(name.node)) |
330 |
val parents_yxml = Symbol.encode_yxml(list(string)(parents)) |
|
331 |
||
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
332 |
val blobs_yxml = |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
333 |
{ |
72745 | 334 |
val encode_blob: T[Exn.Result[Command.Blob]] = |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
335 |
variant(List( |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
336 |
{ case Exn.Res(Command.Blob(a, b, c)) => |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
337 |
(Nil, triple(string, string, option(string))( |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
338 |
(a.node, b.implode, c.map(p => p._1.toString)))) }, |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
339 |
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
340 |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
341 |
Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
342 |
} |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
343 |
|
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
344 |
val toks_yxml = |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
345 |
{ |
64616 | 346 |
val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
347 |
Symbol.encode_yxml(list(encode_tok)(command.span.content)) |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
348 |
} |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
349 |
val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source)) |
59085
08a6901eb035
clarified define_command: send tokens more directly, without requiring keywords in ML;
wenzelm
parents:
58015
diff
changeset
|
350 |
|
72946 | 351 |
(Document_ID(command.id), Symbol.encode(command.span.name), parents_yxml, |
352 |
blobs_yxml, toks_yxml, toks_sources) |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
353 |
} |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
354 |
|
72946 | 355 |
def define_command(resources: Resources, command: Command) |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
356 |
{ |
72946 | 357 |
val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) = |
358 |
encode_command(resources, command) |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
359 |
protocol_command_args( |
72946 | 360 |
"Document.define_command", command_id :: name :: parents_yxml :: blobs_yxml :: |
361 |
toks_yxml :: toks_sources) |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
362 |
} |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
363 |
|
72946 | 364 |
def define_commands(resources: Resources, commands: List[Command]) |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
365 |
{ |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
366 |
protocol_command_args("Document.define_commands", |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
367 |
commands.map(command => |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
368 |
{ |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
369 |
import XML.Encode._ |
72946 | 370 |
val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) = |
371 |
encode_command(resources, command) |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
372 |
val body = |
72946 | 373 |
pair(string, pair(string, pair(string, pair(string, pair(string, list(string))))))( |
374 |
command_id, (name, (parents_yxml, (blobs_yxml, (toks_yxml, toks_sources))))) |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
375 |
YXML.string_of_body(body) |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
376 |
})) |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
377 |
} |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
378 |
|
72946 | 379 |
def define_commands_bulk(resources: Resources, commands: List[Command]) |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
380 |
{ |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
381 |
val (irregular, regular) = commands.partition(command => YXML.detect(command.source)) |
72946 | 382 |
irregular.foreach(define_command(resources, _)) |
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
383 |
regular match { |
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
384 |
case Nil => |
72946 | 385 |
case List(command) => define_command(resources, command) |
386 |
case _ => define_commands(resources, regular) |
|
70664
2bd9e30183b1
prefer define_commands_bulk: fewer protocol messages;
wenzelm
parents:
70661
diff
changeset
|
387 |
} |
54519
5fed81762406
maintain blobs within document state: digest + text in ML, digest-only in Scala;
wenzelm
parents:
54515
diff
changeset
|
388 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
389 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
390 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
391 |
/* execution */ |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
392 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
393 |
def discontinue_execution(): Unit = |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
394 |
protocol_command("Document.discontinue_execution") |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
395 |
|
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
396 |
def cancel_exec(id: Document_ID.Exec): Unit = |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
397 |
protocol_command("Document.cancel_exec", Document_ID(id)) |
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
398 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
399 |
|
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
400 |
/* document versions */ |
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
wenzelm
parents:
46938
diff
changeset
|
401 |
|
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset
|
402 |
def update(old_id: Document_ID.Version, new_id: Document_ID.Version, |
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
403 |
edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
404 |
{ |
69849 | 405 |
val consolidate_yxml = |
406 |
{ |
|
407 |
import XML.Encode._ |
|
408 |
Symbol.encode_yxml(list(string)(consolidate.map(_.node))) |
|
409 |
} |
|
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset
|
410 |
val edits_yxml = |
61376
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
411 |
{ |
93224745477f
output HTML text according to Isabelle/Scala Symbol.Interpretation;
wenzelm
parents:
60992
diff
changeset
|
412 |
import XML.Encode._ |
44383 | 413 |
def id: T[Command] = (cmd => long(cmd.id)) |
46737 | 414 |
def encode_edit(name: Document.Node.Name) |
52849 | 415 |
: T[Document.Node.Edit[Command.Edit, Command.Perspective]] = |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
416 |
variant(List( |
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
417 |
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, |
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
48705
diff
changeset
|
418 |
{ case Document.Node.Deps(header) => |
60992 | 419 |
val master_dir = File.standard_url(name.master_dir) |
70638
f164cec7ac22
clarified signature: prefer operations without position;
wenzelm
parents:
70284
diff
changeset
|
420 |
val imports = header.imports.map(_.node) |
72764 | 421 |
val keywords = header.keywords.map({ case (a, spec) => (a, (spec.kind, spec.tags)) }) |
44979
68b990e950b1
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44866
diff
changeset
|
422 |
(Nil, |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
423 |
pair(string, pair(string, pair(list(string), |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72745
diff
changeset
|
424 |
pair(list(pair(string, pair(string, list(string)))), list(string)))))( |
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65439
diff
changeset
|
425 |
(master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, |
52849 | 426 |
{ case Document.Node.Perspective(a, b, c) => |
427 |
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
428 |
list(pair(id, pair(string, list(string))))(c.dest)) })) |
69849 | 429 |
edits.map({ case (name, edit) => |
430 |
Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) }) |
|
68381
2fd3a6d6ba2e
less wasteful consolidation, based on PIDE front-end state and recent changes;
wenzelm
parents:
68336
diff
changeset
|
431 |
} |
70661 | 432 |
protocol_command_args("Document.update", |
433 |
Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml) |
|
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
434 |
} |
43748 | 435 |
|
44673 | 436 |
def remove_versions(versions: List[Document.Version]) |
437 |
{ |
|
438 |
val versions_yxml = |
|
59364 | 439 |
{ import XML.Encode._ |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65313
diff
changeset
|
440 |
Symbol.encode_yxml(list(long)(versions.map(_.id))) } |
52582 | 441 |
protocol_command("Document.remove_versions", versions_yxml) |
44673 | 442 |
} |
443 |
||
43748 | 444 |
|
50498 | 445 |
/* dialog via document content */ |
446 |
||
52931
ac6648c0c0fb
cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents:
52862
diff
changeset
|
447 |
def dialog_result(serial: Long, result: String): Unit = |
63805 | 448 |
protocol_command("Document.dialog_result", Value.Long(serial), result) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
449 |
} |