author | wenzelm |
Tue, 31 Jan 2023 14:59:19 +0100 | |
changeset 77147 | 38077c938d01 |
parent 77144 | 42c3970e1ac1 |
child 77149 | 3991a35cd740 |
permissions | -rw-r--r-- |
76606 | 1 |
/* Title: Pure/PIDE/document_editor.scala |
2 |
Author: Makarius |
|
3 |
||
76730 | 4 |
Central resources and configuration for interactive document preparation. |
76606 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Document_Editor { |
|
11 |
/* document output */ |
|
12 |
||
13 |
def document_name: String = "document" |
|
14 |
def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output") |
|
15 |
def document_output(): Path = document_output_dir() + Path.basic(document_name) |
|
16 |
||
17 |
def view_document(): Unit = { |
|
18 |
val path = document_output().pdf |
|
19 |
if (path.is_file) Isabelle_System.pdf_viewer(path) |
|
20 |
} |
|
21 |
||
22 |
||
76730 | 23 |
/* configuration state */ |
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
24 |
|
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
25 |
sealed case class Session( |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
26 |
background: Option[Sessions.Background], |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
27 |
selection: Set[Document.Node.Name], |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
28 |
snapshot: Option[Document.Snapshot] |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
29 |
) { |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
30 |
def is_vacuous: Boolean = background.isEmpty |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
31 |
def is_pending: Boolean = snapshot.isEmpty |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
32 |
|
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
33 |
def get_background: Sessions.Background = background.get |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
34 |
def get_variant: Document_Build.Document_Variant = get_background.info.documents.head |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
35 |
def get_snapshot: Document.Snapshot = snapshot.get |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
36 |
} |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
37 |
|
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
38 |
sealed case class State( |
76678 | 39 |
session_background: Option[Sessions.Background] = None, |
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
40 |
selection: Set[Document.Node.Name] = Set.empty, |
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
41 |
views: Set[AnyRef] = Set.empty, |
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
42 |
) { |
76678 | 43 |
def is_active: Boolean = session_background.isDefined && views.nonEmpty |
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
44 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
45 |
def all_document_theories: List[Document.Node.Name] = |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
46 |
session_background match { |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
47 |
case Some(background) => background.base.all_document_theories |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
48 |
case None => Nil |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
49 |
} |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
50 |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
51 |
def active_document_theories: List[Document.Node.Name] = |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
52 |
if (is_active) all_document_theories else Nil |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
53 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
54 |
def select( |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
55 |
names: Iterable[Document.Node.Name], |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
56 |
set: Boolean = false, |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
57 |
toggle: Boolean = false |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
58 |
): State = { |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
59 |
copy(selection = |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
60 |
names.foldLeft(selection) { |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
61 |
case (sel, name) => |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
62 |
val b = if (toggle) !selection(name) else set |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
63 |
if (b) sel + name else sel - name |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
64 |
}) |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
65 |
} |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
66 |
|
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
67 |
def register_view(id: AnyRef): State = copy(views = views + id) |
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
68 |
def unregister_view(id: AnyRef): State = copy(views = views - id) |
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
69 |
|
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
70 |
def session(get_snapshot: () => Document.Snapshot): Session = { |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
71 |
val background = session_background.filter(_.info.documents.nonEmpty) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
72 |
val snapshot = |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
73 |
if (background.isEmpty) None |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
74 |
else { |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
75 |
val snapshot = get_snapshot() |
77147 | 76 |
if (snapshot.is_outdated || !selection.forall(snapshot.document_ready)) None |
77 |
else Some(snapshot) |
|
77144
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
78 |
} |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
79 |
Session(background, selection, snapshot) |
42c3970e1ac1
clarified Document_Editor.Session: more explicit types, more robust operations;
wenzelm
parents:
76994
diff
changeset
|
80 |
} |
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
81 |
} |
76606 | 82 |
} |