author | wenzelm |
Wed, 11 Aug 2010 22:41:26 +0200 | |
changeset 38355 | 8cb265fb12fe |
parent 38220 | b30aa2dbedca |
child 38360 | 53224a4d2f0e |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/command.scala |
2 |
Author: Johannes Hölzl, TU Munich |
|
3 |
Author: Fabian Immler, TU Munich |
|
4 |
Author: Makarius |
|
5 |
||
6 |
Prover commands with semantic state. |
|
7 |
*/ |
|
34407 | 8 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34865
diff
changeset
|
9 |
package isabelle |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
34451 | 11 |
|
34699 | 12 |
import scala.actors.Actor, Actor._ |
34497 | 13 |
import scala.collection.mutable |
34486 | 14 |
|
34451 | 15 |
|
37129 | 16 |
case class Command_Set(set: Set[Command]) |
17 |
||
18 |
||
34637 | 19 |
object Command |
20 |
{ |
|
21 |
object Status extends Enumeration |
|
22 |
{ |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
val UNPROCESSED = Value("UNPROCESSED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
24 |
val FINISHED = Value("FINISHED") |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
25 |
val FAILED = Value("FAILED") |
36990
449628c148cf
explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];
wenzelm
parents:
36676
diff
changeset
|
26 |
val UNDEFINED = Value("UNDEFINED") |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
27 |
} |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
28 |
|
37197
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
29 |
case class HighlightInfo(kind: String, sub_kind: Option[String]) { |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
30 |
override def toString = kind |
953fc4983439
more detailed token markup, including command kind as sub_kind;
wenzelm
parents:
37189
diff
changeset
|
31 |
} |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
32 |
case class TypeInfo(ty: String) |
34707
cc5d388fcbf2
eliminated MarkupInfo, moved particular variants into object Command;
wenzelm
parents:
34705
diff
changeset
|
33 |
case class RefInfo(file: Option[String], line: Option[Int], |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38220
diff
changeset
|
34 |
command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. State_ID !? |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
35 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
36 |
|
34697 | 37 |
class Command( |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
38 |
val id: Document.Command_ID, |
37129 | 39 |
val span: Thy_Syntax.Span, |
38220 | 40 |
val static_parent: Option[Command] = None) // FIXME !? |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
41 |
extends Session.Entity |
34451 | 42 |
{ |
34859 | 43 |
/* classification */ |
34500
384427c750c8
state_results: separate buffer for messages from running command;
wenzelm
parents:
34497
diff
changeset
|
44 |
|
36012 | 45 |
def is_command: Boolean = !span.isEmpty && span.head.is_command |
34865 | 46 |
def is_ignored: Boolean = span.forall(_.is_ignored) |
34859 | 47 |
def is_malformed: Boolean = !is_command && !is_ignored |
48 |
||
36012 | 49 |
def name: String = if (is_command) span.head.content else "" |
37129 | 50 |
override def toString = |
37373
25078ba44436
tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;
wenzelm
parents:
37197
diff
changeset
|
51 |
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
34495 | 52 |
|
34859 | 53 |
|
54 |
/* source text */ |
|
34451 | 55 |
|
34859 | 56 |
val source: String = span.map(_.source).mkString |
57 |
def source(i: Int, j: Int): String = source.substring(i, j) |
|
58 |
def length: Int = source.length |
|
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34835
diff
changeset
|
59 |
|
34859 | 60 |
lazy val symbol_index = new Symbol.Index(source) |
34593 | 61 |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
62 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
63 |
/* accumulated messages */ |
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 |
@volatile protected var state = new State(this) |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
66 |
def current_state: State = state |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
67 |
|
37129 | 68 |
private case class Consume(message: XML.Tree, forward: Command => Unit) |
34832
d785f72ef388
more explicit treatment of command/document state;
wenzelm
parents:
34823
diff
changeset
|
69 |
private case object Assign |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
70 |
|
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
71 |
private val accumulator = actor { |
34832
d785f72ef388
more explicit treatment of command/document state;
wenzelm
parents:
34823
diff
changeset
|
72 |
var assigned = false |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
73 |
loop { |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
74 |
react { |
37129 | 75 |
case Consume(message, forward) if !assigned => |
76 |
val old_state = state |
|
37178
d52f934f8ff6
accumulate only local results -- no proper history support yet;
wenzelm
parents:
37129
diff
changeset
|
77 |
state = old_state.accumulate(message) |
37129 | 78 |
if (!(state eq old_state)) forward(static_parent getOrElse this) |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
79 |
|
34832
d785f72ef388
more explicit treatment of command/document state;
wenzelm
parents:
34823
diff
changeset
|
80 |
case Assign => |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
81 |
assigned = true // single assignment |
34832
d785f72ef388
more explicit treatment of command/document state;
wenzelm
parents:
34823
diff
changeset
|
82 |
reply(()) |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
83 |
|
37189 | 84 |
case bad => System.err.println("Command accumulator: ignoring bad message " + bad) |
34815
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 |
} |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
87 |
} |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
88 |
|
37129 | 89 |
def consume(message: XML.Tree, forward: Command => Unit) |
90 |
{ |
|
91 |
accumulator ! Consume(message, forward) |
|
92 |
} |
|
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
93 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37373
diff
changeset
|
94 |
def assign_state(state_id: Document.State_ID): Command = |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
95 |
{ |
37129 | 96 |
val cmd = new Command(state_id, span, Some(this)) |
34832
d785f72ef388
more explicit treatment of command/document state;
wenzelm
parents:
34823
diff
changeset
|
97 |
accumulator !? Assign |
34815
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
98 |
cmd.state = current_state |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
99 |
cmd |
6bae73cd8e33
unified Command and Command_State, eliminated separate Accumulator;
wenzelm
parents:
34813
diff
changeset
|
100 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
101 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
102 |
|
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
103 |
/* markup */ |
34508 | 104 |
|
34859 | 105 |
lazy val empty_markup = new Markup_Text(Nil, source) |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
106 |
|
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34708
diff
changeset
|
107 |
def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = |
34699 | 108 |
{ |
34703 | 109 |
val start = symbol_index.decode(begin) |
110 |
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
|
111 |
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
|
112 |
} |
34676
9e725d34df7b
Command and Command_State handle results from prover as Accumulator
immler@in.tum.de
parents:
34675
diff
changeset
|
113 |
} |