author  wenzelm 
Wed, 30 Dec 2009 21:57:29 +0100  
changeset 34819  86cb7f8e5a0d 
parent 34818  7df68a8f0e3e 
permissions  rwrr 
34407  1 
/* 
34485  2 
* Document as list of commands, consisting of lists of tokens 
34407  3 
* 
4 
* @author Johannes Hölzl, TU Munich 

34532  5 
* @author Fabian Immler, TU Munich 
34485  6 
* @author Makarius 
34407  7 
*/ 
8 

34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

9 
package isabelle.proofdocument 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

10 

34760  11 

34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

12 
import scala.actors.Actor._ 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

13 

34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

14 
import java.util.regex.Pattern 
34703  15 

34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

16 

34760  17 
object Proof_Document 
34483  18 
{ 
34582  19 
// Be careful when changing this regex. Not only must it handle the 
34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

20 
// spurious end of a token but also: 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

21 
// Bug ID: 5050507 Pattern.matches throws StackOverflow Error 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

22 
// http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507 
34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

23 

7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

24 
val token_pattern = 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

25 
Pattern.compile( 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

26 
"\\{\\*([^*]\\*[^}]\\*\\z)*(\\z\\*\\})" + 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

27 
"\\(\\*([^*]\\*[^)]\\*\\z)*(\\z\\*\\))" + 
34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

28 
"(\\?'?')[AZaz_09.]*" + 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

29 
"[AZaz_09.]+" + 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

30 
"[!#$%&*+/<=>?@^_~]+" + 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

31 
"\"([^\\\\\"]?(\\\\(.\\z))?)*+(\"\\z)" + 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

32 
"`([^\\\\`]?(\\\\(.\\z))?)*+(`\\z)" + 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

33 
"[()\\[\\]{}:;]", Pattern.MULTILINE) 
34485  34 

34808
e462572536e9
eliminated global Session.document_0  did not work due to hardwired id;
wenzelm
parents:
34807
diff
changeset

35 
def empty(id: Isar_Document.Document_ID): Proof_Document = 
34778  36 
new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map()) 
34660  37 

38 
type StructureChange = List[(Option[Command], Option[Command])] 

34778  39 
} 
34538
20bfcca24658
Prover as actor managing ProofDocumentversions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset

40 

34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

41 

34760  42 
class Proof_Document( 
34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

43 
val id: Isar_Document.Document_ID, 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

44 
val tokens: Linear_Set[Token], // FIXME plain List, inside Command 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

45 
val token_start: Map[Token, Int], // FIXME eliminate 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

46 
val commands: Linear_Set[Command], 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

47 
var states: Map[Command, Command]) // FIXME immutable, eliminate!? 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

48 
extends Session.Entity 
34483  49 
{ 
34760  50 
import Proof_Document.StructureChange 
34653  51 

34582  52 
def content = Token.string_from_tokens(Nil ++ tokens, token_start) 
34657  53 

54 

34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

55 
/* accumulated messages */ 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

56 

7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

57 
private val accumulator = actor { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

58 
loop { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

59 
react { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

60 
case (session: Session, message: XML.Tree) => 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

61 
message match { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

62 
case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) => 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

63 
for { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

64 
XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _) 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

65 
< elems 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

66 
} { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

67 
session.lookup_entity(cmd_id) match { 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

68 
case Some(cmd: Command) => 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

69 
val state = cmd.finish_static(state_id) 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

70 
session.register_entity(state) 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

71 
states += (cmd > state) // FIXME !? 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

72 
session.command_change.event(cmd) // FIXME really!? 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

73 
case _ => 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

74 
} 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

75 
} 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

76 
case _ => 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

77 
} 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

78 

7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

79 
case bad => System.err.println("document accumulator: ignoring bad message " + bad) 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

80 
} 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

81 
} 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

82 
} 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

83 

7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

84 
def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) } 
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

85 

7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

86 

7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

87 

34485  88 
/** token view **/ 
89 

34778  90 
def text_changed(session: Session, change: Change): (Proof_Document, StructureChange) = 
34485  91 
{ 
34760  92 
def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = { 
34660  93 
val (doc, chgs) = doc_chgs 
34778  94 
val (new_doc, chg) = doc.text_edit(session, edit, change.id) 
34660  95 
(new_doc, chgs ++ chg) 
96 
} 

34693  97 
((this, Nil: StructureChange) /: change.edits)(edit_doc) 
34660  98 
} 
99 

34778  100 
def text_edit(session: Session, e: Edit, id: String): (Proof_Document, StructureChange) = 
34660  101 
{ 
102 
case class TextChange(start: Int, added: String, removed: String) 

103 
val change = e match { 

104 
case Insert(s, a) => TextChange(s, a, "") 

105 
case Remove(s, r) => TextChange(s, "", r) 

106 
} 

34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

107 
//indices of tokens 
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

108 
var start: Map[Token, Int] = token_start 
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

109 
def stop(t: Token) = start(t) + t.length 
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

110 
// split old token lists 
34582  111 
val tokens = Nil ++ this.tokens 
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

112 
val (begin, remaining) = tokens.span(stop(_) < change.start) 
34648  113 
val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length) 
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

114 
// update indices 
34582  115 
start = end.foldLeft(start)((s, t) => 
34648  116 
s + (t > (s(t) + change.added.length  change.removed.length))) 
34485  117 

34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

118 
val split_begin = removed.takeWhile(start(_) < change.start). 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

119 
map (t => { 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

120 
val split_tok = new Token(t.content.substring(0, change.start  start(t)), t.kind) 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

121 
start += (split_tok > start(t)) 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

122 
split_tok 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

123 
}) 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

124 

34648  125 
val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length). 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

126 
map (t => { 
34582  127 
val split_tok = 
34648  128 
new Token(t.content.substring(change.start + change.removed.length  start(t)), t.kind) 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

129 
start += (split_tok > start(t)) 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

130 
split_tok 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

131 
}) 
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

132 
// update indices 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

133 
start = removed.foldLeft (start) ((s, t) => s  t) 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

134 
start = split_end.foldLeft (start) ((s, t) => 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

135 
s + (t > (change.start + change.added.length))) 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

136 

34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

137 
val ins = new Token(change.added, Token.Kind.OTHER) 
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

138 
start += (ins > change.start) 
34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

139 

34582  140 
var invalid_tokens = split_begin ::: ins :: split_end ::: end 
141 
var new_tokens: List[Token] = Nil 

142 
var old_suffix: List[Token] = Nil 

34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

143 

34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

144 
val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0) 
34582  145 
val matcher = 
34760  146 
Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) 
34526  147 

148 
while (matcher.find() && invalid_tokens != Nil) { 

34485  149 
val kind = 
34819  150 
if (session.current_syntax.is_command(matcher.group)) 
34485  151 
Token.Kind.COMMAND_START 
34494  152 
else if (matcher.end  matcher.start > 2 && matcher.group.substring(0, 2) == "(*") 
34485  153 
Token.Kind.COMMENT 
154 
else 

155 
Token.Kind.OTHER 

34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

156 
val new_token = new Token(matcher.group, kind) 
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset

157 
start += (new_token > (match_start + matcher.start)) 
34526  158 
new_tokens ::= new_token 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

159 

34660  160 
invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token)) 
34526  161 
invalid_tokens match { 
34582  162 
case t :: ts => 
163 
if (start(t) == start(new_token) && 

164 
start(t) > change.start + change.added.length) { 

34597  165 
old_suffix = t :: ts 
34592  166 
new_tokens = new_tokens.tail 
34526  167 
invalid_tokens = Nil 
168 
} 

169 
case _ => 

34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

170 
} 
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

171 
} 
34526  172 
val insert = new_tokens.reverse 
34544
56217d219e27
proofdocumentversions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset

173 
val new_token_list = begin ::: insert ::: old_suffix 
34778  174 
token_changed(session, id, begin.lastOption, insert, 
34597  175 
old_suffix.firstOption, new_token_list, start) 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

176 
} 
34582  177 

34818
7df68a8f0e3e
register Proof_Document instances as session entities  handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset

178 

34485  179 
/** command view **/ 
180 

34582  181 
private def token_changed( 
34778  182 
session: Session, 
34582  183 
new_id: String, 
184 
before_change: Option[Token], 

185 
inserted_tokens: List[Token], 

186 
after_change: Option[Token], 

34597  187 
new_tokens: List[Token], 
34660  188 
new_token_start: Map[Token, Int]): 
34760  189 
(Proof_Document, StructureChange) = 
34485  190 
{ 
34689  191 
val new_tokenset = Linear_Set[Token]() ++ new_tokens 
34593  192 
val cmd_before_change = before_change match { 
193 
case None => None 

194 
case Some(bc) => 

195 
val cmd_with_bc = commands.find(_.contains(bc)).get 

196 
if (cmd_with_bc.tokens.last == bc) { 

197 
if (new_tokenset.next(bc).map(_.is_start).getOrElse(true)) 

198 
Some(cmd_with_bc) 

199 
else commands.prev(cmd_with_bc) 

200 
} 

201 
else commands.prev(cmd_with_bc) 

202 
} 

34544
56217d219e27
proofdocumentversions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset

203 

34593  204 
val cmd_after_change = after_change match { 
205 
case None => None 

206 
case Some(ac) => 

207 
val cmd_with_ac = commands.find(_.contains(ac)).get 

208 
if (ac.is_start) 

209 
Some(cmd_with_ac) 

210 
else 

211 
commands.next(cmd_with_ac) 

212 
} 

34485  213 

34593  214 
val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1). 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

215 
takeWhile(Some(_) != cmd_after_change) 
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

216 

7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

217 
// calculate inserted commands 
34526  218 
def tokens_to_commands(tokens: List[Token]): List[Command]= { 
219 
tokens match { 

220 
case Nil => Nil 

34582  221 
case t :: ts => 
222 
val (cmd, rest) = 

223 
ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT) 

34778  224 
new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest) 
34485  225 
} 
226 
} 

227 

34593  228 
val split_begin = 
229 
if (before_change.isDefined) { 

230 
val changed = 

231 
if (cmd_before_change.isDefined) 

34595  232 
new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1) 
34593  233 
else new_tokenset 
234 
if (changed.exists(_ == before_change.get)) 

34597  235 
changed.takeWhile(_ != before_change.get).toList ::: 
236 
List(before_change.get) 

34593  237 
else Nil 
238 
} else Nil 

34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

239 

34593  240 
val split_end = 
34667  241 
if (after_change.isDefined) { 
34595  242 
val unchanged = new_tokens.dropWhile(_ != after_change.get) 
34667  243 
if(cmd_after_change.isDefined) { 
244 
if (unchanged.exists(_ == cmd_after_change.get.tokens.first)) 

245 
unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList 

246 
else Nil 

247 
} else { 

248 
unchanged 

249 
} 

34593  250 
} else Nil 
251 

34597  252 
val rescan_begin = 
253 
split_begin ::: 

254 
before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens) 

34582  255 
val rescanning_tokens = 
34597  256 
after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) ::: 
257 
split_end 

34593  258 
val inserted_commands = tokens_to_commands(rescanning_tokens.toList) 
34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

259 

34550
171c8c6e5707
prepared proofdocument for only needed changes
immler@in.tum.de
parents:
34544
diff
changeset

260 
// build new document 
34739  261 
val new_commandset = commands. 
262 
delete_between(cmd_before_change, cmd_after_change). 

263 
append_after(cmd_before_change, inserted_commands) 

264 

34554
7dc6c231da40
abs. stops, markup nodes depend on docversion;
immler@in.tum.de
parents:
34551
diff
changeset

265 

34544
56217d219e27
proofdocumentversions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset

266 
val doc = 
34760  267 
new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset, 
34778  268 
states  removed_commands) 
34660  269 

270 
val removes = 

271 
for (cmd < removed_commands) yield (cmd_before_change > None) 

272 
val inserts = 

273 
for (cmd < inserted_commands) yield (doc.commands.prev(cmd) > Some(cmd)) 

274 

275 
return (doc, removes.toList ++ inserts) 

34485  276 
} 
34596  277 

278 
val commands_offsets = { 

279 
var last_stop = 0 

280 
(for (c < commands) yield { 

281 
val r = c > (last_stop,c.stop(this)) 

282 
last_stop = c.stop(this) 

283 
r 

284 
}).toArray 

285 
} 

286 

34712
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

287 
def command_at(pos: Int): Option[Command] = 
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

288 
find_command(pos, 0, commands_offsets.length) 
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

289 

34596  290 
// use a binary search to find commands for a given offset 
34712
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

291 
private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] = 
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

292 
{ 
34596  293 
val middle_index = (array_start + array_stop) / 2 
34712
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

294 
if (middle_index >= commands_offsets.length) return None 
34596  295 
val (middle, (start, stop)) = commands_offsets(middle_index) 
296 
// does middle contain pos? 

34712
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

297 
if (start <= pos && pos < stop) 
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

298 
Some(middle) 
34596  299 
else if (start > pos) 
34712
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

300 
find_command(pos, array_start, middle_index) 
34596  301 
else if (stop <= pos) 
34712
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

302 
find_command(pos, middle_index + 1, array_stop) 
4f0ee5ab0380
replaced find_command_at by command_at  nullfree, proper Option;
wenzelm
parents:
34703
diff
changeset

303 
else error("impossible") 
34596  304 
} 
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset

305 
} 