author | wenzelm |
Fri, 01 Jan 2010 14:41:25 +0100 | |
changeset 34823 | 2f3ea37c5958 |
parent 34815 | 6bae73cd8e33 |
child 34832 | d785f72ef388 |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
2 |
* Prover commands with semantic state |
|
3 |
* |
|
4 |
* @author Johannes Hölzl, TU Munich |
|
5 |
* @author Fabian Immler, TU Munich |
|
6 |
*/ |
|
7 |
||
34760 | 8 |
package isabelle.proofdocument |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
34451 | 10 |
|
34699 | 11 |
import scala.actors.Actor, Actor._ |
34497 | 12 |
import scala.collection.mutable |
34486 | 13 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34769
diff
changeset
|
14 |
import isabelle.jedit.Isabelle |
34675 | 15 |
|
34451 | 16 |
|
34637 | 17 |
object Command |
18 |
{ |
|
19 |
object Status extends Enumeration |
|
20 |
{ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
21 |
val UNPROCESSED = Value("UNPROCESSED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
22 |
val FINISHED = Value("FINISHED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
val FAILED = Value("FAILED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
24 |
} |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
25 |
|
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
26 |
case class HighlightInfo(highlight: String) { override def toString = highlight } |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
27 |
case class TypeInfo(ty: String) |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
28 |
case class RefInfo(file: Option[String], line: Option[Int], |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
29 |
command_id: Option[String], offset: Option[Int]) |
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 |
|
34451 | 32 |
|
34697 | 33 |
class Command( |
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34778
diff
changeset
|
34 |
val id: Isar_Document.Command_ID, |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
35 |
val tokens: List[Token], |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
36 |
val starts: Map[Token, Int]) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
37 |
extends Session.Entity |
34451 | 38 |
{ |
34637 | 39 |
require(!tokens.isEmpty) |
40 |
||
34813
f0107bc96961
more explicit modeling of Command and Command_State as Session.Entity;
wenzelm
parents:
34778
diff
changeset
|
41 |
// FIXME override equality as well |
34653 | 42 |
override def hashCode = id.hashCode |
34637 | 43 |
|
34674 | 44 |
|
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
45 |
/* content */ |
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
46 |
|
34495 | 47 |
override def toString = name |
48 |
||
34526 | 49 |
val name = tokens.head.content |
34582 | 50 |
val content: String = Token.string_from_tokens(tokens, starts) |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
51 |
def content(i: Int, j: Int): String = content.substring(i, j) |
34637 | 52 |
val symbol_index = new Symbol.Index(content) |
34451 | 53 |
|
34823 | 54 |
def start(doc: Document) = doc.token_start(tokens.first) |
55 |
def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length |
|
34451 | 56 |
|
34593 | 57 |
def contains(p: Token) = tokens.contains(p) |
58 |
||
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
59 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
60 |
/* accumulated messages */ |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
61 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
62 |
@volatile protected var state = new State(this) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
63 |
def current_state: State = state |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
64 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
65 |
private case class Consume(session: Session, message: XML.Tree) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
66 |
private case object Finish |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
67 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
68 |
private val accumulator = actor { |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
69 |
var finished = false |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
70 |
loop { |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
71 |
react { |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
72 |
case Consume(session: Session, message: XML.Tree) if !finished => |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
73 |
state = state.+(session, message) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
74 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
75 |
case Finish => finished = true; reply(()) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
76 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
77 |
case bad => System.err.println("command accumulator: ignoring bad message " + bad) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
78 |
} |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
79 |
} |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
80 |
} |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
81 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
82 |
def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) } |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
83 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
84 |
def finish_static(state_id: Isar_Document.State_ID): Command = |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
85 |
{ |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
86 |
val cmd = new Command(state_id, tokens, starts) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
87 |
accumulator !? Finish |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
88 |
cmd.state = current_state |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
89 |
cmd |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
90 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
91 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
92 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
93 |
/* markup */ |
34508 | 94 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
95 |
lazy val empty_markup = new Markup_Text(Nil, content) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
96 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
97 |
def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = |
34699 | 98 |
{ |
34703 | 99 |
val start = symbol_index.decode(begin) |
100 |
val stop = symbol_index.decode(end) |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
101 |
new Markup_Tree(new Markup_Node(start, stop, info), Nil) |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
102 |
} |
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
103 |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
104 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
105 |
/* results, markup, etc. */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
106 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
107 |
def results: List[XML.Tree] = current_state.results |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
108 |
def markup_root: Markup_Text = current_state.markup_root |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
109 |
def type_at(pos: Int): Option[String] = current_state.type_at(pos) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
110 |
def ref_at(pos: Int): Option[Markup_Node] = current_state.ref_at(pos) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
111 |
def highlight: Markup_Text = current_state.highlight |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
112 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
113 |
|
34823 | 114 |
private def cmd_state(doc: Document): State = // FIXME clarify |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
115 |
doc.states.getOrElse(this, this).current_state |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
116 |
|
34823 | 117 |
def status(doc: Document) = cmd_state(doc).status |
118 |
def results(doc: Document) = cmd_state(doc).results |
|
119 |
def markup_root(doc: Document) = cmd_state(doc).markup_root |
|
120 |
def highlight(doc: Document) = cmd_state(doc).highlight |
|
121 |
def type_at(doc: Document, offset: Int) = cmd_state(doc).type_at(offset) |
|
122 |
def ref_at(doc: Document, offset: Int) = cmd_state(doc).ref_at(offset) |
|
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
123 |
} |