author | wenzelm |
Fri, 16 Mar 2018 15:22:08 +0100 | |
changeset 67877 | ff12c4556e2f |
parent 67869 | 8cb4fef58379 |
child 67879 | e4903b803b8b |
permissions | -rw-r--r-- |
67054 | 1 |
/* Title: Pure/Thy/thy_resources.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
PIDE resources for theory files. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Thy_Resources |
|
11 |
{ |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
12 |
/* PIDE session */ |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
13 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
14 |
def start_session( |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
15 |
options: Options, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
16 |
session_name: String, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
17 |
session_dirs: List[Path] = Nil, |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
18 |
session_base: Option[Sessions.Base] = None, |
67869 | 19 |
print_mode: List[String] = Nil, |
20 |
progress: Progress = No_Progress, |
|
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
21 |
log: Logger = No_Logger): Session = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
22 |
{ |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
23 |
val base = |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
24 |
session_base getOrElse |
67852
f701a1d5d852
allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
wenzelm
parents:
67064
diff
changeset
|
25 |
Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
26 |
val resources = new Thy_Resources(base, log = log) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
27 |
val session = new Session(options, resources) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
28 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
29 |
val session_error = Future.promise[String] |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
30 |
var session_phase: Session.Consumer[Session.Phase] = null |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
31 |
session_phase = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
32 |
Session.Consumer(getClass.getName) { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
33 |
case Session.Ready => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
34 |
session.phase_changed -= session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
35 |
session_error.fulfill("") |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
36 |
case Session.Terminated(result) if !result.ok => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
37 |
session.phase_changed -= session_phase |
67869 | 38 |
session_error.fulfill("Session start failed: return code " + result.rc) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
39 |
case _ => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
40 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
41 |
session.phase_changed += session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
42 |
|
67877 | 43 |
progress.echo("Starting " + session_name + " ...") |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
44 |
Isabelle_Process.start(session, options, |
67869 | 45 |
logic = session_name, dirs = session_dirs, modes = print_mode) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
46 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
47 |
session_error.join match { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
48 |
case "" => session |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
49 |
case msg => session.stop(); error(msg) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
50 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
51 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
52 |
|
67063 | 53 |
class Session private[Thy_Resources]( |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
54 |
session_options: Options, |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
55 |
override val resources: Thy_Resources) extends isabelle.Session(session_options, resources) |
67063 | 56 |
{ |
57 |
session => |
|
58 |
||
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
59 |
def use_theories( |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
60 |
theories: List[(String, Position.T)], |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
61 |
qualifier: String = Sessions.DRAFT, |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
62 |
master_dir: String = ""): (List[Document.Node.Name], Document.State) = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
63 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
64 |
val requirements = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
65 |
resources.load_theories(session, theories, qualifier = qualifier, master_dir = master_dir) |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
66 |
val state = consolidated_state(requirements) |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
67 |
(requirements, state) |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
68 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
69 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
70 |
def consolidated_state(requirements: List[Document.Node.Name]): Document.State = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
71 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
72 |
val promise = Future.promise[Document.State] |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
73 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
74 |
def check_state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
75 |
{ |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
76 |
val state = session.current_state() |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
77 |
state.stable_tip_version match { |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
78 |
case Some(version) if requirements.forall(state.node_consolidated(version, _)) => |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
79 |
try { promise.fulfill(state) } |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
80 |
catch { case _: IllegalStateException => } |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
81 |
case _ => |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
82 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
83 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
84 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
85 |
val consumer = |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
86 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
87 |
case changed => if (requirements.exists(changed.nodes)) check_state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
88 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
89 |
|
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
90 |
session.commands_changed += consumer |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
91 |
check_state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
92 |
val state = promise.join |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
93 |
session.commands_changed -= consumer |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
94 |
state |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
95 |
} |
67063 | 96 |
} |
97 |
||
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
98 |
|
67054 | 99 |
/* internal state */ |
100 |
||
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
101 |
sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
102 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
103 |
final class Theory private[Thy_Resources]( |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
104 |
val node_name: Document.Node.Name, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
105 |
val node_header: Document.Node.Header, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
106 |
val text: String) |
67056 | 107 |
{ |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
108 |
override def toString: String = node_name.toString |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
109 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
110 |
def node_perspective: Document.Node.Perspective_Text = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
111 |
Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
112 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
113 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
114 |
{ |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
115 |
val text_edits = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
116 |
if (old.isEmpty) Text.Edit.inserts(0, text) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
117 |
else Text.Edit.replace(0, old.get.text, text) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
118 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
119 |
if (text_edits.isEmpty) Nil |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
120 |
else |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
121 |
List(node_name -> Document.Node.Deps(node_header), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
122 |
node_name -> Document.Node.Edits(text_edits), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
123 |
node_name -> node_perspective) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
124 |
} |
67056 | 125 |
} |
67054 | 126 |
} |
127 |
||
67056 | 128 |
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) |
67054 | 129 |
extends Resources(session_base, log = log) |
130 |
{ |
|
67056 | 131 |
resources => |
132 |
||
67054 | 133 |
private val state = Synchronized(Thy_Resources.State()) |
67056 | 134 |
|
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
135 |
def read_thy(node_name: Document.Node.Name): Thy_Resources.Theory = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
136 |
{ |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
137 |
val path = node_name.path |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
138 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
139 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
140 |
val text = File.read(path) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
141 |
val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
142 |
new Thy_Resources.Theory(node_name, node_header, text) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
143 |
} |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
144 |
|
67056 | 145 |
def load_theories( |
146 |
session: Session, |
|
147 |
theories: List[(String, Position.T)], |
|
148 |
qualifier: String = Sessions.DRAFT, |
|
149 |
master_dir: String = ""): List[Document.Node.Name] = |
|
150 |
{ |
|
151 |
val import_names = |
|
152 |
for ((thy, pos) <- theories) |
|
153 |
yield (import_name(qualifier, master_dir, thy), pos) |
|
154 |
||
155 |
val dependencies = resources.dependencies(import_names).check_errors |
|
67059 | 156 |
val loaded_theories = dependencies.theories.map(read_thy(_)) |
67056 | 157 |
|
158 |
val edits = |
|
159 |
state.change_result(st => |
|
160 |
{ |
|
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
161 |
val theory_edits = |
67056 | 162 |
for { |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
163 |
theory <- loaded_theories |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
164 |
node_name = theory.node_name |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
165 |
edits = theory.node_edits(st.theories.get(node_name)) |
67056 | 166 |
if edits.nonEmpty |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
167 |
} yield ((node_name, theory), edits) |
67056 | 168 |
|
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
169 |
val st1 = st.copy(theories = st.theories ++ theory_edits.map(_._1)) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
170 |
(theory_edits.flatMap(_._2), st1) |
67056 | 171 |
}) |
172 |
session.update(Document.Blobs.empty, edits) |
|
173 |
||
67059 | 174 |
dependencies.theories |
67056 | 175 |
} |
67054 | 176 |
} |