author | wenzelm |
Wed, 21 Dec 2022 14:00:00 +0100 | |
changeset 76730 | 1b8dd8c0492f |
parent 76716 | a7602257a825 |
child 76732 | 0ba6f360d38a |
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 |
||
23 |
/* progress */ |
|
24 |
||
25 |
class Log_Progress(session: Session) extends Progress { |
|
26 |
def show(text: String): Unit = {} |
|
27 |
||
28 |
private val syslog = session.make_syslog() |
|
29 |
||
30 |
private def update(text: String = syslog.content()): Unit = show(text) |
|
76610 | 31 |
private val delay = Delay.first(session.update_delay, gui = true) { update() } |
76606 | 32 |
|
33 |
override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } |
|
34 |
||
35 |
def load(): Unit = GUI_Thread.require { |
|
36 |
val path = document_output().log |
|
37 |
val text = if (path.is_file) File.read(path) else "" |
|
38 |
GUI_Thread.later { delay.revoke(); update(text) } |
|
39 |
} |
|
40 |
||
41 |
GUI_Thread.later { update() } |
|
42 |
} |
|
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
43 |
|
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
44 |
|
76730 | 45 |
/* configuration state */ |
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
46 |
|
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
47 |
sealed case class State( |
76678 | 48 |
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
|
49 |
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
|
50 |
views: Set[AnyRef] = Set.empty, |
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
51 |
) { |
76678 | 52 |
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
|
53 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
54 |
def is_required(name: Document.Node.Name): Boolean = |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
55 |
is_active && selection.contains(name) && all_document_theories.contains(name) |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
56 |
|
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
57 |
def required: List[Document.Node.Name] = |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
58 |
if (is_active) all_document_theories.filter(selection) else Nil |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
59 |
|
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
60 |
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
|
61 |
session_background match { |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
62 |
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
|
63 |
case None => Nil |
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 |
|
76716
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
66 |
def active_document_theories: List[Document.Node.Name] = |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
67 |
if (is_active) all_document_theories else Nil |
a7602257a825
clarified state document nodes for Theories_Status / Document_Dockable;
wenzelm
parents:
76715
diff
changeset
|
68 |
|
76715
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
69 |
def select( |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
70 |
names: Iterable[Document.Node.Name], |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
71 |
set: Boolean = false, |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
72 |
toggle: Boolean = false |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
73 |
): State = { |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
74 |
copy(selection = |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
75 |
names.foldLeft(selection) { |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
76 |
case (sel, name) => |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
77 |
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
|
78 |
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
|
79 |
}) |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
80 |
} |
bf5ff407f32f
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
wenzelm
parents:
76678
diff
changeset
|
81 |
|
76609
cc9ddf373bd2
maintain global state of document editor views, notably for is_active operation;
wenzelm
parents:
76606
diff
changeset
|
82 |
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
|
83 |
def unregister_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
|
84 |
} |
76606 | 85 |
} |