author | paulson <lp15@cam.ac.uk> |
Wed, 24 Apr 2024 20:56:26 +0100 | |
changeset 80149 | 40a3fc07a587 |
parent 78614 | 4da5cdaa4dcd |
permissions | -rw-r--r-- |
62973 | 1 |
/* Title: Tools/jEdit/src/jedit_sessions.scala |
49246 | 2 |
Author: Makarius |
3 |
||
65256 | 4 |
Isabelle/jEdit session information, based on implicit process environment |
5 |
and explicit options. |
|
49246 | 6 |
*/ |
7 |
||
8 |
package isabelle.jedit |
|
9 |
||
10 |
||
11 |
import isabelle._ |
|
12 |
||
13 |
||
75393 | 14 |
object JEdit_Sessions { |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
15 |
/* session options */ |
62972 | 16 |
|
73367 | 17 |
def session_dirs: List[Path] = |
70382
23ba5a638e6d
more robust: avoid folding of jEdit file-names wrt. JEDIT_SESSION_DIRS;
wenzelm
parents:
70105
diff
changeset
|
18 |
Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-") |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
19 |
|
73367 | 20 |
def session_no_build: Boolean = |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
21 |
Isabelle_System.getenv("JEDIT_NO_BUILD") == "true" |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
22 |
|
75393 | 23 |
def session_options(options: Options): Options = { |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
24 |
val options1 = |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
25 |
Isabelle_System.getenv("JEDIT_BUILD_MODE") match { |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
26 |
case "default" => options |
70105 | 27 |
case mode => options.bool.update("system_heaps", mode == "system") |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
28 |
} |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
29 |
|
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
30 |
val options2 = |
77483 | 31 |
Isabelle_System.getenv("JEDIT_PROCESS_POLICY") match { |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
32 |
case "" => options1 |
77483 | 33 |
case s => options1.string.update("process_policy", s) |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
34 |
} |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
35 |
|
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
36 |
options2 |
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
37 |
} |
69853
f7c9a1be333f
more uniform session_system_mode (see also e57416b649d5);
wenzelm
parents:
69758
diff
changeset
|
38 |
|
75817 | 39 |
def sessions_structure( |
40 |
options: Options = PIDE.options.value, |
|
41 |
dirs: List[Path] = session_dirs |
|
42 |
): Sessions.Structure = { |
|
69758 | 43 |
Sessions.load_structure(session_options(options), dirs = dirs) |
75817 | 44 |
} |
69758 | 45 |
|
77022 | 46 |
|
47 |
/* database store */ |
|
48 |
||
78178 | 49 |
def sessions_store(options: Options = PIDE.options.value): Store = |
50 |
Store(session_options(options)) |
|
76728 | 51 |
|
77022 | 52 |
def open_session_context( |
78178 | 53 |
store: Store = sessions_store(), |
77022 | 54 |
session_background: Sessions.Background = PIDE.resources.session_background, |
55 |
document_snapshot: Option[Document.Snapshot] = None |
|
56 |
): Export.Session_Context = { |
|
57 |
Export.open_session_context(store, session_background, document_snapshot = document_snapshot) |
|
58 |
} |
|
59 |
||
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
60 |
|
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
61 |
/* raw logic info */ |
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
62 |
|
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
63 |
private val jedit_logic_option = "jedit_logic" |
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
64 |
|
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
65 |
def logic_name(options: Options): String = |
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
66 |
Isabelle_System.default_logic( |
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
67 |
Isabelle_System.getenv("JEDIT_LOGIC"), |
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
68 |
options.string(jedit_logic_option)) |
64602 | 69 |
|
66988 | 70 |
def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) |
68370 | 71 |
def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" |
68541 | 72 |
def logic_include_sessions: List[String] = |
73 |
space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) |
|
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
74 |
|
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
75 |
def logic_info(options: Options): Option[Sessions.Info] = |
75817 | 76 |
try { sessions_structure(options = options).get(logic_name(options)) } |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
77 |
catch { case ERROR(_) => None } |
64602 | 78 |
|
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
79 |
def logic_root(options: Options): Position.T = |
68370 | 80 |
if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
81 |
else Position.none |
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
82 |
|
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
83 |
|
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
84 |
/* session selectors */ |
66979 | 85 |
|
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
86 |
class Selector( |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
87 |
val options: Options_Variable, |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
88 |
val option_name: String, |
76580 | 89 |
standalone: Boolean, |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
90 |
batches: List[GUI.Selector.Entry[String]]*) |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
91 |
extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry { |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
92 |
name = option_name |
76581 | 93 |
tooltip = |
78614 | 94 |
if (standalone) Word.capitalized(options.value.description(option_name)) |
76581 | 95 |
else options.value.check_name(option_name).print_default |
66979 | 96 |
|
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
97 |
override val title: String = |
76579 | 98 |
options.value.check_name(option_name).title_jedit |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
99 |
override def load(): Unit = { |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
100 |
val value = options.string(option_name) |
77183 | 101 |
for (entry <- find_value(_ == value) if selection.item != entry) { |
102 |
selection.item = entry |
|
103 |
} |
|
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
104 |
} |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
105 |
override def save(): Unit = |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
106 |
for (value <- selection_value) options.string(option_name) = value |
75829 | 107 |
|
76580 | 108 |
override def changed(): Unit = if (standalone) save() |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
109 |
|
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
110 |
load() |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
111 |
} |
76492
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76391
diff
changeset
|
112 |
|
76679 | 113 |
def logic_selector(options: Options_Variable, standalone: Boolean = false): Selector = |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
114 |
GUI_Thread.require { |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
115 |
val sessions = sessions_structure(options = options.value) |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
116 |
val all_sessions = sessions.imports_topological_order |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
117 |
val main_sessions = all_sessions.filter(name => sessions(name).main_group) |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
118 |
|
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
119 |
val default_entry = |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
120 |
GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")") |
76492
e228be7cd375
clarified GUI.Selector, with support for separator as pseudo-entry;
wenzelm
parents:
76391
diff
changeset
|
121 |
|
76580 | 122 |
new Selector(options, jedit_logic_option, standalone, |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
123 |
default_entry :: main_sessions.map(GUI.Selector.item), |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
124 |
all_sessions.sorted.map(GUI.Selector.item)) |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
125 |
} |
75828 | 126 |
|
76679 | 127 |
def document_selector(options: Options_Variable, standalone: Boolean = false): Selector = |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
128 |
GUI_Thread.require { |
76742 | 129 |
val sessions = sessions_structure(options = options.value + "document") |
130 |
val all_sessions = |
|
131 |
sessions.build_topological_order.filter(name => sessions(name).documents.nonEmpty).sorted |
|
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
132 |
val doc_sessions = all_sessions.filter(name => sessions(name).doc_group) |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
133 |
|
76580 | 134 |
new Selector(options, "editor_document_session", standalone, |
76578
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
135 |
doc_sessions.map(GUI.Selector.item), |
06b001094ddb
more uniform session selectors, with persistent options;
wenzelm
parents:
76504
diff
changeset
|
136 |
all_sessions.map(GUI.Selector.item)) |
66979 | 137 |
} |
138 |
||
139 |
||
140 |
/* session build process */ |
|
64602 | 141 |
|
76656 | 142 |
def session_background(options: Options): Sessions.Background = |
143 |
Sessions.background(options, |
|
73367 | 144 |
dirs = JEdit_Sessions.session_dirs, |
68541 | 145 |
include_sessions = logic_include_sessions, |
68370 | 146 |
session = logic_name(options), |
147 |
session_ancestor = logic_ancestor, |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70382
diff
changeset
|
148 |
session_requirements = logic_requirements) |
65571 | 149 |
|
65256 | 150 |
def session_build( |
75393 | 151 |
options: Options, |
152 |
progress: Progress = new Progress, |
|
153 |
no_build: Boolean = false |
|
154 |
): Int = { |
|
71981 | 155 |
Build.build(session_options(options), |
75752 | 156 |
selection = Sessions.Selection.session(PIDE.resources.session_base.session_name), |
73367 | 157 |
progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs, |
76656 | 158 |
infos = PIDE.resources.session_background.infos).rc |
62972 | 159 |
} |
160 |
||
76728 | 161 |
def session_start(options: Options): Unit = { |
71604 | 162 |
val session = PIDE.session |
76656 | 163 |
val session_background = PIDE.resources.session_background |
77022 | 164 |
val store = sessions_store(options = options) |
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77183
diff
changeset
|
165 |
val session_heaps = |
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77183
diff
changeset
|
166 |
ML_Process.session_heaps(store, session_background, logic = session_background.session_name) |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69853
diff
changeset
|
167 |
|
71604 | 168 |
session.phase_changed += PIDE.plugin.session_phase_changed |
169 |
||
77414
0d5994eef9e6
clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;
wenzelm
parents:
77183
diff
changeset
|
170 |
Isabelle_Process.start(store.options, session, session_background, session_heaps, |
66973
829c3133c4ca
added isabelle jedit options -B, -P, clarified -R;
wenzelm
parents:
66965
diff
changeset
|
171 |
modes = |
76728 | 172 |
(space_explode(',', store.options.string("jedit_print_mode")) ::: |
71604 | 173 |
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse) |
62972 | 174 |
} |
49246 | 175 |
} |