author | wenzelm |
Tue, 07 Sep 2010 16:40:30 +0200 | |
changeset 39172 | 31b95e0da7b7 |
parent 39170 | 04ad0fed81f5 |
child 39175 | a08d68e993ea |
permissions | -rw-r--r-- |
38483 | 1 |
/* Title: Pure/PIDE/isar_document.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 |
|
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
4 |
Protocol message formats for interactive Isar 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 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
10 |
object Isar_Document |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
11 |
{ |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
12 |
/* document editing */ |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
13 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
14 |
object Assign { |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
15 |
def unapply(msg: XML.Tree) |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
16 |
: Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] = |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
17 |
msg match { |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
18 |
case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) => |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
19 |
val id_edits = edits.map(Edit.unapply) |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
20 |
if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get))) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
21 |
else None |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
22 |
case _ => None |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
23 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
24 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
25 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
26 |
object Edit { |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
27 |
def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
28 |
msg match { |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
29 |
case XML.Elem( |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
30 |
Markup(Markup.EDIT, |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
31 |
List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j)) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
32 |
case _ => None |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
33 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
34 |
} |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
35 |
|
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
36 |
|
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
37 |
/* toplevel transactions */ |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
38 |
|
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
39 |
sealed abstract class Status |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
40 |
case class Forked(forks: Int) extends Status |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
41 |
case object Unprocessed extends Status |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
42 |
case object Finished extends Status |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
43 |
case object Failed extends Status |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
44 |
|
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38567
diff
changeset
|
45 |
def command_status(markup: List[Markup]): Status = |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
46 |
{ |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
47 |
val forks = (0 /: markup) { |
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38567
diff
changeset
|
48 |
case (i, Markup(Markup.FORKED, _)) => i + 1 |
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38567
diff
changeset
|
49 |
case (i, Markup(Markup.JOINED, _)) => i - 1 |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
50 |
case (i, _) => i |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
51 |
} |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
52 |
if (forks != 0) Forked(forks) |
38581
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38567
diff
changeset
|
53 |
else if (markup.exists(_.name == Markup.FAILED)) Failed |
d503a0912e14
simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);
wenzelm
parents:
38567
diff
changeset
|
54 |
else if (markup.exists(_.name == Markup.FINISHED)) Finished |
38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
55 |
else Unprocessed |
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset
|
56 |
} |
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
|
57 |
|
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
|
58 |
|
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
|
59 |
/* reported positions */ |
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
|
60 |
|
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
61 |
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) |
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
62 |
private val exclude_pos = Set(Markup.LOCATION) |
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
63 |
|
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
64 |
private def is_state(msg: XML.Tree): Boolean = |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
65 |
msg match { |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
66 |
case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
67 |
case _ => false |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
68 |
} |
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
69 |
|
39172
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
70 |
def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] = |
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
|
71 |
{ |
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
|
72 |
def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = |
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
|
73 |
tree match { |
39172
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
74 |
case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body) |
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
75 |
if include_pos(name) && id == command.id => |
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
76 |
val range = command.decode(raw_range).restrict(command.range) |
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
77 |
body.foldLeft(if (range.is_singularity) set else set + range)(reported) |
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
78 |
case XML.Elem(Markup(name, _), body) if !exclude_pos(name) => |
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
79 |
body.foldLeft(set)(reported) |
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
80 |
case _ => set |
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
|
81 |
} |
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
82 |
val set = reported(Set.empty, message) |
39170
04ad0fed81f5
Isar_Document.reported_positions: exclude proof state output;
wenzelm
parents:
39042
diff
changeset
|
83 |
if (set.isEmpty && !is_state(message)) |
39172
31b95e0da7b7
Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;
wenzelm
parents:
39170
diff
changeset
|
84 |
set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) |
39042
470fd769ae53
Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;
wenzelm
parents:
38887
diff
changeset
|
85 |
else set |
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
|
86 |
} |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
87 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
88 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
89 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
90 |
trait Isar_Document extends Isabelle_Process |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
91 |
{ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
92 |
import Isar_Document._ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
93 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
94 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
95 |
/* commands */ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
96 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
97 |
def define_command(id: Document.Command_ID, text: String): Unit = |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
98 |
input("Isar_Document.define_command", Document.ID(id), text) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
99 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
100 |
|
38417 | 101 |
/* document versions */ |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
102 |
|
38417 | 103 |
def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
104 |
edits: List[Document.Edit[Document.Command_ID]]) |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
105 |
{ |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
106 |
val arg = |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
107 |
XML_Data.make_list( |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
108 |
XML_Data.make_pair(XML_Data.make_string)( |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
109 |
XML_Data.make_option(XML_Data.make_list( |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38418
diff
changeset
|
110 |
XML_Data.make_pair( |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38418
diff
changeset
|
111 |
XML_Data.make_option(XML_Data.make_long))( |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38418
diff
changeset
|
112 |
XML_Data.make_option(XML_Data.make_long))))))(edits) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
113 |
|
38417 | 114 |
input("Isar_Document.edit_version", |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38412
diff
changeset
|
115 |
Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
116 |
} |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
117 |
} |