author | wenzelm |
Sun, 15 Aug 2010 14:18:52 +0200 | |
changeset 38417 | b8922ae21111 |
parent 38374 | 7eb0f6991e25 |
child 38419 | f9dc924e54f8 |
permissions | -rw-r--r-- |
34268 | 1 |
/* Title: Pure/Thy/thy_syntax.scala |
2 |
Author: Makarius |
|
3 |
||
38374 | 4 |
Superficial theory syntax: tokens and spans. |
34268 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
38239
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
10 |
import scala.collection.mutable |
38374 | 11 |
import scala.annotation.tailrec |
38239
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
12 |
|
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
13 |
|
34303 | 14 |
object Thy_Syntax |
34268 | 15 |
{ |
38374 | 16 |
/** parse spans **/ |
17 |
||
38373 | 18 |
def parse_spans(toks: List[Token]): List[List[Token]] = |
34268 | 19 |
{ |
38373 | 20 |
val result = new mutable.ListBuffer[List[Token]] |
38239
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
21 |
val span = new mutable.ListBuffer[Token] |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
22 |
val whitespace = new mutable.ListBuffer[Token] |
34268 | 23 |
|
38239
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
24 |
def flush(buffer: mutable.ListBuffer[Token]) |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
25 |
{ |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
26 |
if (!buffer.isEmpty) { result += buffer.toList; buffer.clear } |
34268 | 27 |
} |
38239
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
28 |
for (tok <- toks) { |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
29 |
if (tok.is_command) { flush(span); flush(whitespace); span += tok } |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
30 |
else if (tok.is_ignored) whitespace += tok |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
31 |
else { span ++= whitespace; whitespace.clear; span += tok } |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
32 |
} |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
33 |
flush(span); flush(whitespace) |
89a4d1028fb3
parse_spans: somewhat faster low-level implementation;
wenzelm
parents:
36956
diff
changeset
|
34 |
result.toList |
34268 | 35 |
} |
38374 | 36 |
|
37 |
||
38 |
||
39 |
/** text edits **/ |
|
40 |
||
38417 | 41 |
def text_edits(session: Session, previous: Document.Version, |
42 |
edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) = |
|
38374 | 43 |
{ |
44 |
/* phase 1: edit individual command source */ |
|
45 |
||
46 |
@tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]) |
|
47 |
: Linear_Set[Command] = |
|
48 |
{ |
|
49 |
eds match { |
|
50 |
case e :: es => |
|
51 |
Document.Node.command_starts(commands.iterator).find { |
|
52 |
case (cmd, cmd_start) => |
|
53 |
e.can_edit(cmd.source, cmd_start) || |
|
54 |
e.is_insert && e.start == cmd_start + cmd.length |
|
55 |
} match { |
|
56 |
case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => |
|
57 |
val (rest, text) = e.edit(cmd.source, cmd_start) |
|
58 |
val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd |
|
59 |
edit_text(rest.toList ::: es, new_commands) |
|
60 |
||
61 |
case Some((cmd, cmd_start)) => |
|
62 |
edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text))) |
|
63 |
||
64 |
case None => |
|
65 |
require(e.is_insert && e.start == 0) |
|
66 |
edit_text(es, commands.insert_after(None, Command.unparsed(e.text))) |
|
67 |
} |
|
68 |
case Nil => commands |
|
69 |
} |
|
70 |
} |
|
71 |
||
72 |
||
73 |
/* phase 2: recover command spans */ |
|
74 |
||
75 |
@tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] = |
|
76 |
{ |
|
77 |
commands.iterator.find(_.is_unparsed) match { |
|
78 |
case Some(first_unparsed) => |
|
79 |
val first = |
|
80 |
commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head |
|
81 |
val last = |
|
82 |
commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last |
|
83 |
val range = |
|
84 |
commands.iterator(first).takeWhile(_ != last).toList ::: List(last) |
|
85 |
||
86 |
val sources = range.flatMap(_.span.map(_.source)) |
|
87 |
val spans0 = parse_spans(session.current_syntax.scan(sources.mkString)) |
|
88 |
||
89 |
val (before_edit, spans1) = |
|
90 |
if (!spans0.isEmpty && first.is_command && first.span == spans0.head) |
|
91 |
(Some(first), spans0.tail) |
|
92 |
else (commands.prev(first), spans0) |
|
93 |
||
94 |
val (after_edit, spans2) = |
|
95 |
if (!spans1.isEmpty && last.is_command && last.span == spans1.last) |
|
96 |
(Some(last), spans1.take(spans1.length - 1)) |
|
97 |
else (commands.next(last), spans1) |
|
98 |
||
99 |
val inserted = spans2.map(span => new Command(session.create_id(), span)) |
|
100 |
val new_commands = |
|
101 |
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) |
|
102 |
recover_spans(new_commands) |
|
103 |
||
104 |
case None => commands |
|
105 |
} |
|
106 |
} |
|
107 |
||
108 |
||
109 |
/* resulting document edits */ |
|
110 |
||
111 |
{ |
|
112 |
val doc_edits = new mutable.ListBuffer[Document.Edit[Command]] |
|
38417 | 113 |
var nodes = previous.nodes |
38374 | 114 |
|
115 |
for ((name, text_edits) <- edits) { |
|
116 |
val commands0 = nodes(name).commands |
|
117 |
val commands1 = edit_text(text_edits, commands0) |
|
118 |
val commands2 = recover_spans(commands1) // FIXME somewhat slow |
|
119 |
||
120 |
val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList |
|
121 |
val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList |
|
122 |
||
123 |
val cmd_edits = |
|
124 |
removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) ::: |
|
125 |
inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd))) |
|
126 |
||
127 |
doc_edits += (name -> Some(cmd_edits)) |
|
128 |
nodes += (name -> new Document.Node(commands2)) |
|
129 |
} |
|
38417 | 130 |
(doc_edits.toList, new Document.Version(session.create_id(), nodes)) |
38374 | 131 |
} |
132 |
} |
|
34268 | 133 |
} |