author | wenzelm |
Sun, 12 Nov 2017 20:17:29 +0100 | |
changeset 67062 | ee0823ce2828 |
parent 67061 | 2efa25302f34 |
child 67063 | 10d608cc7470 |
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, |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
19 |
modes: List[String] = Nil, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
20 |
log: Logger = No_Logger): Session = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
21 |
{ |
67062
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
22 |
val base = |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
23 |
session_base getOrElse |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
24 |
Sessions.base_info(options, session_name, dirs = session_dirs).check_base |
ee0823ce2828
optional session_base, e.g. from existing Sessions.Deps in build.scala;
wenzelm
parents:
67061
diff
changeset
|
25 |
val resources = new Thy_Resources(base, log = log) |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
26 |
val session = new Session(options, resources) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
27 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
28 |
val session_error = Future.promise[String] |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
29 |
var session_phase: Session.Consumer[Session.Phase] = null |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
30 |
session_phase = |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
31 |
Session.Consumer(getClass.getName) { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
32 |
case Session.Ready => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
33 |
session.phase_changed -= session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
34 |
session_error.fulfill("") |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
35 |
case Session.Terminated(result) if !result.ok => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
36 |
session.phase_changed -= session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
37 |
session_error.fulfill("Prover startup failed: return code " + result.rc) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
38 |
case _ => |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
39 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
40 |
session.phase_changed += session_phase |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
41 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
42 |
Isabelle_Process.start(session, options, |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
43 |
logic = session_name, dirs = session_dirs, modes = modes) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
44 |
|
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
45 |
session_error.join match { |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
46 |
case "" => session |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
47 |
case msg => session.stop(); error(msg) |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
48 |
} |
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
49 |
} |
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 |
|
67054 | 52 |
/* internal state */ |
53 |
||
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
54 |
sealed case class State(theories: Map[Document.Node.Name, Theory] = Map.empty) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
55 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
56 |
final class Theory private[Thy_Resources]( |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
57 |
val node_name: Document.Node.Name, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
58 |
val node_header: Document.Node.Header, |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
59 |
val text: String) |
67056 | 60 |
{ |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
61 |
override def toString: String = node_name.toString |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
62 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
63 |
def node_perspective: Document.Node.Perspective_Text = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
64 |
Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
65 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
66 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
67 |
{ |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
68 |
val text_edits = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
69 |
if (old.isEmpty) Text.Edit.inserts(0, text) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
70 |
else Text.Edit.replace(0, old.get.text, text) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
71 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
72 |
if (text_edits.isEmpty) Nil |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
73 |
else |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
74 |
List(node_name -> Document.Node.Deps(node_header), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
75 |
node_name -> Document.Node.Edits(text_edits), |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
76 |
node_name -> node_perspective) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
77 |
} |
67056 | 78 |
} |
67054 | 79 |
} |
80 |
||
67056 | 81 |
class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) |
67054 | 82 |
extends Resources(session_base, log = log) |
83 |
{ |
|
67056 | 84 |
resources => |
85 |
||
67054 | 86 |
private val state = Synchronized(Thy_Resources.State()) |
67056 | 87 |
|
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
88 |
def read_thy(node_name: Document.Node.Name): Thy_Resources.Theory = |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
89 |
{ |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
90 |
val path = node_name.path |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
91 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
92 |
|
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
93 |
val text = File.read(path) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
94 |
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
|
95 |
new Thy_Resources.Theory(node_name, node_header, text) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
96 |
} |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
97 |
|
67056 | 98 |
def load_theories( |
99 |
session: Session, |
|
100 |
theories: List[(String, Position.T)], |
|
101 |
qualifier: String = Sessions.DRAFT, |
|
102 |
master_dir: String = ""): List[Document.Node.Name] = |
|
103 |
{ |
|
104 |
val import_names = |
|
105 |
for ((thy, pos) <- theories) |
|
106 |
yield (import_name(qualifier, master_dir, thy), pos) |
|
107 |
||
108 |
val dependencies = resources.dependencies(import_names).check_errors |
|
67059 | 109 |
val loaded_theories = dependencies.theories.map(read_thy(_)) |
67056 | 110 |
|
111 |
val edits = |
|
112 |
state.change_result(st => |
|
113 |
{ |
|
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
114 |
val theory_edits = |
67056 | 115 |
for { |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
116 |
theory <- loaded_theories |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
117 |
node_name = theory.node_name |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
118 |
edits = theory.node_edits(st.theories.get(node_name)) |
67056 | 119 |
if edits.nonEmpty |
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
120 |
} yield ((node_name, theory), edits) |
67056 | 121 |
|
67058
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
122 |
val st1 = st.copy(theories = st.theories ++ theory_edits.map(_._1)) |
03d4954c68bb
simplified: eliminated pointless Thy_Document_Model;
wenzelm
parents:
67057
diff
changeset
|
123 |
(theory_edits.flatMap(_._2), st1) |
67056 | 124 |
}) |
125 |
session.update(Document.Blobs.empty, edits) |
|
126 |
||
67059 | 127 |
dependencies.theories |
67056 | 128 |
} |
67054 | 129 |
} |