--- a/.hgtags Fri Apr 10 22:50:59 2020 +0100
+++ b/.hgtags Fri Apr 10 22:51:18 2020 +0100
@@ -41,3 +41,4 @@
7eadccd4392cc1f3b603c0fa5734d0629f039cc0 Isabelle2020-RC2
7fe1a344404a9f7e6e4cdef584338c6d9849812c Isabelle2020-RC3
1f3d9a9dd42a9543af7062ca08a36da2c5375454 Isabelle2020-RC4
+8ed68b2aeba19ea47f1e38038ac87a32c17161ce Isabelle2020-RC5
--- a/NEWS Fri Apr 10 22:50:59 2020 +0100
+++ b/NEWS Fri Apr 10 22:51:18 2020 +0100
@@ -12,6 +12,17 @@
* The command-line tool "isabelle console" now supports interrupts
properly (on Linux and macOS).
+* The Isabelle/Scala "Progress" interface changed slightly and
+"No_Progress" has been discontinued. INCOMPATIBILITY, use "new Progress"
+instead.
+
+* General support for Isabelle/Scala system services, configured via the
+shell function "isabelle_scala_service" in etc/settings (e.g. of an
+Isabelle component); see implementations of class
+Isabelle_System.Service in Isabelle/Scala. This supersedes former
+"isabelle_scala_tools" and "isabelle_file_format": minor
+INCOMPATIBILITY.
+
New in Isabelle2020 (April 2020)
--- a/etc/settings Fri Apr 10 22:50:59 2020 +0100
+++ b/etc/settings Fri Apr 10 22:51:18 2020 +0100
@@ -20,10 +20,10 @@
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-isabelle_scala_tools 'isabelle.Tools'
-[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_tools 'isabelle.Admin_Tools'
+isabelle_scala_service 'isabelle.Tools'
+[ -d "$ISABELLE_HOME/Admin" ] && isabelle_scala_service 'isabelle.Admin_Tools'
-isabelle_file_format 'isabelle.Bibtex$File_Format'
+isabelle_scala_service 'isabelle.Bibtex$File_Format'
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
--- a/lib/scripts/getfunctions Fri Apr 10 22:50:59 2020 +0100
+++ b/lib/scripts/getfunctions Fri Apr 10 22:51:18 2020 +0100
@@ -113,22 +113,6 @@
}
export -f classpath
-#Isabelle/Scala tools
-function isabelle_scala_tools ()
-{
- local X=""
- for X in "$@"
- do
- if [ -z "$ISABELLE_SCALA_TOOLS" ]; then
- ISABELLE_SCALA_TOOLS="$X"
- else
- ISABELLE_SCALA_TOOLS="$ISABELLE_SCALA_TOOLS:$X"
- fi
- done
- export ISABELLE_SCALA_TOOLS
-}
-export -f isabelle_scala_tools
-
#Isabelle fonts
function isabelle_fonts ()
{
@@ -160,21 +144,21 @@
}
export -f isabelle_fonts_hidden
-#file formats
-function isabelle_file_format ()
+#Isabelle/Scala services
+function isabelle_scala_service ()
{
local X=""
for X in "$@"
do
- if [ -z "$ISABELLE_FILE_FORMATS" ]; then
- ISABELLE_FILE_FORMATS="$X"
+ if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
+ ISABELLE_SCALA_SERVICES="$X"
else
- ISABELLE_FILE_FORMATS="$ISABELLE_FILE_FORMATS:$X"
+ ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
fi
done
- export ISABELLE_FILE_FORMATS
+ export ISABELLE_SCALA_SERVICES
}
-export -f isabelle_file_format
+export -f isabelle_scala_service
#administrative build
if [ -e "$ISABELLE_HOME/Admin/build" ]; then
--- a/src/HOL/Data_Structures/AVL_Set.thy Fri Apr 10 22:50:59 2020 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy Fri Apr 10 22:51:18 2020 +0100
@@ -127,13 +127,13 @@
text \<open>First, a fast but relatively manual proof with many lemmas:\<close>
lemma height_balL:
- "\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
+ "\<lbrakk> avl l; avl r; height l = height r + 2 \<rbrakk> \<Longrightarrow>
height (balL l a r) = height r + 2 \<or>
height (balL l a r) = height r + 3"
by (cases l) (auto simp:node_def balL_def split:tree.split)
lemma height_balR:
- "\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow>
+ "\<lbrakk> avl l; avl r; height r = height l + 2 \<rbrakk> \<Longrightarrow>
height (balR l a r) = height l + 2 \<or>
height (balR l a r) = height l + 3"
by (cases r) (auto simp add:node_def balR_def split:tree.split)
@@ -141,61 +141,25 @@
lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
by (simp add: node_def)
-lemma avl_node:
- "\<lbrakk> avl l; avl r;
- height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1
- \<rbrakk> \<Longrightarrow> avl(node l a r)"
-by (auto simp add:max_def node_def)
-
lemma height_balL2:
"\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow>
- height (balL l a r) = (1 + max (height l) (height r))"
+ height (balL l a r) = 1 + max (height l) (height r)"
by (cases l, cases r) (simp_all add: balL_def)
lemma height_balR2:
"\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow>
- height (balR l a r) = (1 + max (height l) (height r))"
+ height (balR l a r) = 1 + max (height l) (height r)"
by (cases l, cases r) (simp_all add: balR_def)
lemma avl_balL:
- assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1
- \<or> height r = height l + 1 \<or> height l = height r + 2"
- shows "avl(balL l a r)"
-proof(cases l rule: tree2_cases)
- case Leaf
- with assms show ?thesis by (simp add: node_def balL_def)
-next
- case Node
- with assms show ?thesis
- proof(cases "height l = height r + 2")
- case True
- from True Node assms show ?thesis
- by (auto simp: balL_def intro!: avl_node split: tree.split) arith+
- next
- case False
- with assms show ?thesis by (simp add: avl_node balL_def)
- qed
-qed
+ "\<lbrakk> avl l; avl r; height r - 1 \<le> height l \<and> height l \<le> height r + 2 \<rbrakk> \<Longrightarrow> avl(balL l a r)"
+by(cases l, cases r)
+ (auto simp: balL_def node_def split!: if_split tree.split)
lemma avl_balR:
- assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1
- \<or> height r = height l + 1 \<or> height r = height l + 2"
- shows "avl(balR l a r)"
-proof(cases r rule: tree2_cases)
- case Leaf
- with assms show ?thesis by (simp add: node_def balR_def)
-next
- case Node
- with assms show ?thesis
- proof(cases "height r = height l + 2")
- case True
- from True Node assms show ?thesis
- by (auto simp: balR_def intro!: avl_node split: tree.split) arith+
- next
- case False
- with assms show ?thesis by (simp add: balR_def avl_node)
- qed
-qed
+ "\<lbrakk> avl l; avl r; height l - 1 \<le> height r \<and> height r \<le> height l + 2 \<rbrakk> \<Longrightarrow> avl(balR l a r)"
+by(cases r, cases l)
+ (auto simp: balR_def node_def split!: if_split tree.split)
text\<open>Insertion maintains the AVL property. Requires simultaneous proof.\<close>
@@ -269,31 +233,19 @@
theorem avl_insert_auto: "avl t \<Longrightarrow>
avl(insert x t) \<and> height (insert x t) \<in> {height t, height t + 1}"
apply (induction t rule: tree2_induct)
- apply (auto split!: if_splits)
- apply (auto simp: balL_def balR_def node_def max_absorb2 split!: tree.splits)
+ (* if you want to save a few secs: apply (auto split!: if_split) *)
+ apply (auto simp: balL_def balR_def node_def max_absorb2 split!: if_split tree.split)
done
subsubsection \<open>Deletion maintains AVL balance\<close>
lemma avl_split_max:
- assumes "avl x" and "x \<noteq> Leaf"
- shows "avl (fst (split_max x))" "height x = height(fst (split_max x)) \<or>
- height x = height(fst (split_max x)) + 1"
-using assms
-proof (induct x rule: split_max_induct)
- case Node
- case 1
- thus ?case using Node
- by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
-next
- case (Node l a _ r)
- case 2
- let ?r' = "fst (split_max r)"
- from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all
- thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a]
- apply (auto split:prod.splits simp del:avl.simps) by arith+
-qed auto
+ "\<lbrakk> avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
+ avl (fst (split_max t)) \<and>
+ height t \<in> {height(fst (split_max t)), height(fst (split_max t)) + 1}"
+by(induct t rule: split_max_induct)
+ (auto simp: balL_def node_def max_absorb2 split!: prod.split if_split tree.split)
text\<open>Deletion maintains the AVL property:\<close>
@@ -304,19 +256,8 @@
proof (induct t rule: tree2_induct)
case (Node l a n r)
case 1
- show ?case
- proof(cases "x = a")
- case True with Node 1 show ?thesis
- using avl_split_max[of l] by (auto simp: avl_balR split: prod.split)
- next
- case False
- show ?thesis
- proof(cases "x<a")
- case True with Node 1 show ?thesis by (auto simp add:avl_balR)
- next
- case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL)
- qed
- qed
+ thus ?case
+ using Node avl_split_max[of l] by (auto simp: avl_balL avl_balR split: prod.split)
case 2
show ?case
proof(cases "x = a")
@@ -363,6 +304,37 @@
qed
qed simp_all
+text \<open>A more automatic proof.
+Complete automation as for insertion seems hard due to resource requirements.\<close>
+
+theorem avl_delete_auto:
+ assumes "avl t"
+ shows "avl(delete x t)" and "height t \<in> {height (delete x t), height (delete x t) + 1}"
+using assms
+proof (induct t rule: tree2_induct)
+ case (Node l a n r)
+ case 1
+ show ?case
+ proof(cases "x = a")
+ case True thus ?thesis
+ using 1 avl_split_max[of l] by (auto simp: avl_balR split: prod.split)
+ next
+ case False thus ?thesis
+ using Node 1 by (auto simp: avl_balL avl_balR)
+ qed
+ case 2
+ show ?case
+ proof(cases "x = a")
+ case True thus ?thesis
+ using 1 avl_split_max[of l]
+ by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split)
+ next
+ case False thus ?thesis
+ using height_balL[of l "delete x r" a] height_balR[of "delete x l" r a] Node 1
+ by(auto simp: balL_def balR_def split!: if_split)
+ qed
+qed simp_all
+
subsection "Overall correctness"
--- a/src/Pure/Admin/build_doc.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_doc.scala Fri Apr 10 22:51:18 2020 +0100
@@ -16,7 +16,7 @@
def build_doc(
options: Options,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
all_docs: Boolean = false,
max_jobs: Int = 1,
docs: List[String] = Nil): Int =
--- a/src/Pure/Admin/build_fonts.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_fonts.scala Fri Apr 10 22:51:18 2020 +0100
@@ -216,7 +216,7 @@
target_prefix: String = "Isabelle",
target_version: String = "",
target_dir: Path = default_target_dir,
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
progress.echo("Directory " + target_dir)
hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
--- a/src/Pure/Admin/build_history.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_history.scala Fri Apr 10 22:51:18 2020 +0100
@@ -106,7 +106,7 @@
options: Options,
root: Path,
user_home: Path = default_user_home,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
rev: String = default_rev,
afp_rev: Option[String] = None,
afp_partition: Int = 0,
@@ -519,7 +519,7 @@
afp_repos_source: String = AFP.repos_source,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
rev: String = "",
afp_rev: Option[String] = None,
options: String = "",
--- a/src/Pure/Admin/build_jdk.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_jdk.scala Fri Apr 10 22:51:18 2020 +0100
@@ -133,7 +133,7 @@
def build_jdk(
archives: List[Path],
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
target_dir: Path = Path.current)
{
if (Platform.is_windows) error("Cannot build jdk on Windows")
--- a/src/Pure/Admin/build_polyml.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_polyml.scala Fri Apr 10 22:51:18 2020 +0100
@@ -49,7 +49,7 @@
def build_polyml(
root: Path,
sha1_root: Option[Path] = None,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
arch_64: Boolean = false,
options: List[String] = Nil,
msys_root: Option[Path] = None)
--- a/src/Pure/Admin/build_release.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_release.scala Fri Apr 10 22:51:18 2020 +0100
@@ -265,7 +265,7 @@
def build_release(base_dir: Path,
options: Options,
components_base: Path = Components.default_components_base,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
rev: String = "",
afp_rev: String = "",
official_release: Boolean = false,
--- a/src/Pure/Admin/build_status.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/build_status.scala Fri Apr 10 22:51:18 2020 +0100
@@ -49,7 +49,7 @@
/* build status */
def build_status(options: Options,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
verbose: Boolean = false,
@@ -200,7 +200,7 @@
}
def read_data(options: Options,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
ml_statistics: Boolean = false,
@@ -362,7 +362,7 @@
/* present data */
def present_data(data: Data,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
target_dir: Path = default_target_dir,
image_size: (Int, Int) = default_image_size)
{
--- a/src/Pure/Admin/components.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/components.scala Fri Apr 10 22:51:18 2020 +0100
@@ -45,7 +45,7 @@
def contrib(dir: Path = Path.current, name: String = ""): Path =
dir + Path.explode("contrib") + Path.explode(name)
- def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
+ def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String =
{
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
@@ -56,7 +56,7 @@
def resolve(base_dir: Path, names: List[String],
target_dir: Option[Path] = None,
copy_dir: Option[Path] = None,
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
Isabelle_System.mkdirs(base_dir)
for (name <- names) {
@@ -135,7 +135,7 @@
def build_components(
options: Options,
components: List[Path],
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
publish: Boolean = false,
force: Boolean = false,
update_components_sha1: Boolean = false)
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Apr 10 22:51:18 2020 +0100
@@ -394,7 +394,7 @@
object Log_Service
{
- def apply(options: Options, progress: Progress = No_Progress): Log_Service =
+ def apply(options: Options, progress: Progress = new Progress): Log_Service =
new Log_Service(SSH.init_context(options), progress)
}
@@ -599,7 +599,7 @@
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = if (verbose) new Console_Progress() else No_Progress
+ val progress = if (verbose) new Console_Progress() else new Progress
if (force) cronjob(progress, exclude_task)
else error("Need to apply force to do anything")
--- a/src/Pure/Admin/jenkins.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/jenkins.scala Fri Apr 10 22:51:18 2020 +0100
@@ -40,7 +40,7 @@
def download_logs(
- options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
+ options: Options, job_names: List[String], dir: Path, progress: Progress = new Progress)
{
val store = Sessions.store(options)
val infos = job_names.flatMap(build_job_infos)
@@ -96,7 +96,7 @@
}
}
- def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
+ def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress)
{
val log_dir = dir + Build_Log.log_subdir(date)
val log_path = log_dir + log_filename.ext("xz")
--- a/src/Pure/Admin/other_isabelle.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Fri Apr 10 22:51:18 2020 +0100
@@ -12,7 +12,7 @@
def apply(isabelle_home: Path,
isabelle_identifier: String = "",
user_home: Path = Path.explode("$USER_HOME"),
- progress: Progress = No_Progress): Other_Isabelle =
+ progress: Progress = new Progress): Other_Isabelle =
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
}
--- a/src/Pure/General/mercurial.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/General/mercurial.scala Fri Apr 10 22:51:18 2020 +0100
@@ -230,7 +230,7 @@
remote_name: String = "",
path_name: String = default_path_name,
remote_exists: Boolean = false,
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
/* local repository */
--- a/src/Pure/Isar/subgoal.ML Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Isar/subgoal.ML Fri Apr 10 22:51:18 2020 +0100
@@ -44,6 +44,7 @@
fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
let
val st = raw_st
+ |> Thm.solve_constraints
|> Thm.transfer' ctxt
|> Raw_Simplifier.norm_hhf_protect ctxt;
val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
--- a/src/Pure/PIDE/headless.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Apr 10 22:51:18 2020 +0100
@@ -244,7 +244,7 @@
// commit: must not block, must not fail
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
commit_cleanup_delay: Time = default_commit_cleanup_delay,
- progress: Progress = No_Progress): Use_Theories_Result =
+ progress: Progress = new Progress): Use_Theories_Result =
{
val dependencies =
{
@@ -404,7 +404,7 @@
session_name: String,
session_dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
log: Logger = No_Logger): Resources =
{
val base_info =
@@ -567,7 +567,7 @@
/* session */
- def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
+ def start_session(print_mode: List[String] = Nil, progress: Progress = new Progress): Session =
{
val session = new Session(session_base_info.session, options, resources)
--- a/src/Pure/PIDE/protocol_handlers.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala Fri Apr 10 22:51:18 2020 +0100
@@ -51,7 +51,10 @@
def init(name: String): State =
{
val new_handler =
- try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
+ try {
+ Some(Class.forName(name).getDeclaredConstructor().newInstance()
+ .asInstanceOf[Session.Protocol_Handler])
+ }
catch { case exn: Throwable => bad_handler(exn, name); None }
new_handler match { case Some(handler) => init(handler) case None => this }
}
--- a/src/Pure/PIDE/resources.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Apr 10 22:51:18 2020 +0100
@@ -23,19 +23,17 @@
/* file formats */
- val file_formats: File_Format.Environment = File_Format.environment()
-
def make_theory_name(name: Document.Node.Name): Option[Document.Node.Name] =
- file_formats.get(name).flatMap(_.make_theory_name(resources, name))
+ File_Format.registry.get(name).flatMap(_.make_theory_name(resources, name))
def make_theory_content(thy_name: Document.Node.Name): Option[String] =
- file_formats.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
+ File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
- file_formats.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
+ File_Format.registry.get(snapshot.node_name).flatMap(_.make_preview(snapshot))
def is_hidden(name: Document.Node.Name): Boolean =
- !name.is_theory || name.theory == Sessions.root_name || file_formats.is_theory(name)
+ !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
def thy_path(path: Path): Path = path.ext("thy")
@@ -265,10 +263,10 @@
def dependencies(
thys: List[(Document.Node.Name, Position.T)],
- progress: Progress = No_Progress): Dependencies[Unit] =
+ progress: Progress = new Progress): Dependencies[Unit] =
Dependencies.empty[Unit].require_thys((), thys, progress = progress)
- def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress)
+ def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
: Dependencies[Options] =
{
(Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
@@ -303,7 +301,7 @@
def require_thy(adjunct: A,
thy: (Document.Node.Name, Position.T),
initiators: List[Document.Node.Name] = Nil,
- progress: Progress = No_Progress): Dependencies[A] =
+ progress: Progress = new Progress): Dependencies[A] =
{
val (name, pos) = thy
@@ -337,7 +335,7 @@
def require_thys(adjunct: A,
thys: List[(Document.Node.Name, Position.T)],
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
(this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
--- a/src/Pure/PIDE/session.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/PIDE/session.scala Fri Apr 10 22:51:18 2020 +0100
@@ -354,7 +354,7 @@
/* file formats */
lazy val file_formats: File_Format.Session =
- resources.file_formats.start_session(session)
+ File_Format.registry.start_session(session)
/* protocol handlers */
--- a/src/Pure/System/isabelle_system.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Apr 10 22:51:18 2020 +0100
@@ -46,16 +46,28 @@
/** implicit settings environment **/
+ abstract class Service
+
@volatile private var _settings: Option[Map[String, String]] = None
+ @volatile private var _services: Option[List[Service]] = None
+
+ private def uninitialized: Boolean = _services.isEmpty // unsynchronized check
def settings(): Map[String, String] =
{
- if (_settings.isEmpty) init() // unsynchronized check
+ if (uninitialized) init()
_settings.get
}
- def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized {
- if (_settings.isEmpty) {
+ def services(): List[Service] =
+ {
+ if (uninitialized) init()
+ _services.get
+ }
+
+ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
+ {
+ if (uninitialized) {
val isabelle_root1 =
bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
@@ -124,12 +136,32 @@
}
_settings = Some(settings)
set_cygwin_root()
+
+ val variable = "ISABELLE_SCALA_SERVICES"
+ val services =
+ for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
+ yield {
+ def err(msg: String): Nothing =
+ error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
+ try {
+ Class.forName(name).asInstanceOf[Class[Service]]
+ .getDeclaredConstructor().newInstance()
+ }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
+ }
+ _services = Some(services)
}
}
/* getenv */
+ private def getenv_error(name: String): Nothing =
+ error("Undefined Isabelle environment variable: " + quote(name))
+
def getenv(name: String, env: Map[String, String] = settings()): String =
env.getOrElse(name, "")
@@ -365,24 +397,6 @@
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
- /* classes */
-
- def init_classes[A](variable: String): List[A] =
- {
- for (name <- space_explode(':', Isabelle_System.getenv_strict(variable)))
- yield {
- def err(msg: String): Nothing =
- error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
-
- try { Class.forName(name).asInstanceOf[Class[A]].newInstance() }
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- }
-
-
/* default logic */
def default_logic(args: String*): String =
--- a/src/Pure/System/isabelle_tool.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala Fri Apr 10 22:51:18 2020 +0100
@@ -98,8 +98,7 @@
/* internal tools */
private lazy val internal_tools: List[Isabelle_Tool] =
- Isabelle_System.init_classes[Isabelle_Scala_Tools]("ISABELLE_SCALA_TOOLS")
- .flatMap(_.tools.toList)
+ Isabelle_System.services.collect { case c: Isabelle_Scala_Tools => c.tools.toList }.flatten
private def list_internal(): List[(String, String)] =
for (tool <- internal_tools.toList)
@@ -140,7 +139,7 @@
sealed case class Isabelle_Tool(name: String, description: String, body: List[String] => Unit)
-class Isabelle_Scala_Tools(val tools: Isabelle_Tool*)
+class Isabelle_Scala_Tools(val tools: Isabelle_Tool*) extends Isabelle_System.Service
class Tools extends Isabelle_Scala_Tools(
Build.isabelle_tool,
--- a/src/Pure/System/linux.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/System/linux.scala Fri Apr 10 22:51:18 2020 +0100
@@ -62,12 +62,12 @@
def check_reboot_required(): Unit =
if (reboot_required()) error("Reboot required")
- def package_update(progress: Progress = No_Progress): Unit =
+ def package_update(progress: Progress = new Progress): Unit =
progress.bash(
"""apt-get update -y && apt-get upgrade -y && apt autoremove -y""",
echo = true).check
- def package_install(packages: List[String], progress: Progress = No_Progress): Unit =
+ def package_install(packages: List[String], progress: Progress = new Progress): Unit =
progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
def package_installed(name: String): Boolean =
--- a/src/Pure/System/progress.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/System/progress.scala Fri Apr 10 22:51:18 2020 +0100
@@ -36,8 +36,15 @@
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
Timing.timeit(message, enabled, echo)(e)
- def stopped: Boolean = false
- def interrupt_handler[A](e: => A): A = e
+ @volatile protected var is_stopped = false
+ def stop { is_stopped = true }
+ def stopped: Boolean =
+ {
+ if (Thread.interrupted) is_stopped = true
+ is_stopped
+ }
+
+ def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
@@ -55,8 +62,6 @@
}
}
-object No_Progress extends Progress
-
class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
{
override def echo(msg: String): Unit =
@@ -64,15 +69,6 @@
override def theory(theory: Progress.Theory): Unit =
if (verbose) echo(theory.message)
-
- @volatile private var is_stopped = false
- override def interrupt_handler[A](e: => A): A =
- POSIX_Interrupt.handler { is_stopped = true } { e }
- override def stopped: Boolean =
- {
- if (Thread.interrupted) is_stopped = true
- is_stopped
- }
}
class File_Progress(path: Path, verbose: Boolean = false) extends Progress
--- a/src/Pure/Thy/export.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Thy/export.scala Fri Apr 10 22:51:18 2020 +0100
@@ -299,7 +299,7 @@
store: Sessions.Store,
session_name: String,
export_dir: Path,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
export_prune: Int = 0,
export_list: Boolean = false,
export_patterns: List[String] = Nil)
--- a/src/Pure/Thy/export_theory.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala Fri Apr 10 22:51:18 2020 +0100
@@ -30,7 +30,7 @@
store: Sessions.Store,
sessions_structure: Sessions.Structure,
session_name: String,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
cache: Term.Cache = Term.make_cache()): Session =
{
val thys =
--- a/src/Pure/Thy/file_format.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Thy/file_format.scala Fri Apr 10 22:51:18 2020 +0100
@@ -12,12 +12,12 @@
sealed case class Theory_Context(name: Document.Node.Name, content: String)
- /* environment */
+ /* registry */
- def environment(): Environment =
- new Environment(Isabelle_System.init_classes[File_Format]("ISABELLE_FILE_FORMATS"))
+ lazy val registry: Registry =
+ new Registry(Isabelle_System.services.collect { case c: File_Format => c })
- final class Environment private [File_Format](file_formats: List[File_Format])
+ final class Registry private [File_Format](file_formats: List[File_Format])
{
override def toString: String = file_formats.mkString("File_Format.Environment(", ",", ")")
@@ -53,10 +53,10 @@
object No_Agent extends Agent
}
-trait File_Format
+trait File_Format extends Isabelle_System.Service
{
def format_name: String
- override def toString: String = format_name
+ override def toString: String = "File_Format(" + format_name + ")"
def file_ext: String
def detect(name: String): Boolean = name.endsWith("." + file_ext)
--- a/src/Pure/Thy/sessions.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Apr 10 22:51:18 2020 +0100
@@ -116,7 +116,7 @@
}
def deps(sessions_structure: Structure,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
inlined_files: Boolean = false,
verbose: Boolean = false,
list_files: Boolean = false,
@@ -345,7 +345,7 @@
def base_info(options: Options,
session: String,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
dirs: List[Path] = Nil,
include_sessions: List[String] = Nil,
session_ancestor: Option[String] = None,
@@ -708,7 +708,7 @@
def selection_deps(
options: Options,
selection: Selection,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
loading_sessions: Boolean = false,
inlined_files: Boolean = false,
verbose: Boolean = false): Deps =
--- a/src/Pure/Tools/build.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/build.scala Fri Apr 10 22:51:18 2020 +0100
@@ -461,7 +461,7 @@
def build(
options: Options,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
check_unknown_files: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
@@ -594,8 +594,7 @@
def sleep()
{
- try { Time.seconds(0.5).sleep }
- catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
+ Isabelle_Thread.interrupt_handler(_ => progress.stop) { Time.seconds(0.5).sleep }
}
val numa_nodes = new NUMA.Nodes(numa_shuffling)
@@ -611,8 +610,9 @@
if (pending.is_empty) results
else {
- if (progress.stopped)
+ if (progress.stopped) {
for ((_, (_, job)) <- running) job.terminate
+ }
running.find({ case (_, (_, job)) => job.is_finished }) match {
case Some((session_name, (input_heaps, job))) =>
@@ -749,7 +749,7 @@
progress.echo_warning("Nothing to build")
Map.empty[String, Result]
}
- else loop(queue, Map.empty, Map.empty)
+ else Isabelle_Thread.uninterruptible { loop(queue, Map.empty, Map.empty) }
val results =
new Results(
@@ -763,7 +763,7 @@
progress.echo("Exporting " + info.name + " ...")
for ((dir, prune, pats) <- info.export_files) {
Export.export_files(store, name, info.dir + dir,
- progress = if (verbose) progress else No_Progress,
+ progress = if (verbose) progress else new Progress,
export_prune = prune,
export_patterns = pats)
}
@@ -937,7 +937,7 @@
/* build logic image */
def build_logic(options: Options, logic: String,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
build_heap: Boolean = false,
dirs: List[Path] = Nil,
fresh: Boolean = false,
--- a/src/Pure/Tools/dump.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/dump.scala Fri Apr 10 22:51:18 2020 +0100
@@ -94,7 +94,7 @@
def apply(
options: Options,
aspects: List[Aspect] = Nil,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
selection: Sessions.Selection = Sessions.Selection.empty,
@@ -395,7 +395,7 @@
options: Options,
logic: String,
aspects: List[Aspect] = Nil,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
--- a/src/Pure/Tools/mkroot.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/mkroot.scala Fri Apr 10 22:51:18 2020 +0100
@@ -25,7 +25,7 @@
init_repos: Boolean = false,
title: String = "",
author: String = "",
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
Isabelle_System.mkdirs(session_dir)
--- a/src/Pure/Tools/phabricator.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/phabricator.scala Fri Apr 10 22:51:18 2020 +0100
@@ -193,7 +193,7 @@
command
}
- def mercurial_setup(mercurial_source: String, progress: Progress = No_Progress)
+ def mercurial_setup(mercurial_source: String, progress: Progress = new Progress)
{
progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
Isabelle_System.with_tmp_dir("mercurial")(tmp_dir =>
@@ -226,7 +226,7 @@
repo: String = "",
package_update: Boolean = false,
mercurial_source: String = "",
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
/* system environment */
@@ -599,7 +599,7 @@
name: String = default_name,
config_file: Option[Path] = None,
test_user: String = "",
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
Linux.check_system_root()
@@ -717,7 +717,7 @@
def phabricator_setup_ssh(
server_port: Int = default_server_port,
system_port: Int = default_system_port,
- progress: Progress = No_Progress)
+ progress: Progress = new Progress)
{
Linux.check_system_root()
--- a/src/Pure/Tools/server.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/server.scala Fri Apr 10 22:51:18 2020 +0100
@@ -274,10 +274,6 @@
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
}
- @volatile private var is_stopped = false
- override def stopped: Boolean = is_stopped
- def stop { is_stopped = true }
-
override def toString: String = context.toString
}
--- a/src/Pure/Tools/server_commands.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala Fri Apr 10 22:51:18 2020 +0100
@@ -45,7 +45,7 @@
include_sessions = include_sessions, verbose = verbose)
}
- def command(args: Args, progress: Progress = No_Progress)
+ def command(args: Args, progress: Progress = new Progress)
: (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
{
val options = Options.init(prefs = args.preferences, opts = args.options)
@@ -103,7 +103,7 @@
}
yield Args(build = build, print_mode = print_mode)
- def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
+ def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger)
: (JSON.Object.T, (UUID.T, Headless.Session)) =
{
val (_, _, options, base_info) =
@@ -179,7 +179,7 @@
def command(args: Args,
session: Headless.Session,
id: UUID.T = UUID.random(),
- progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
+ progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
{
val result =
session.use_theories(args.theories, master_dir = args.master_dir,
--- a/src/Pure/Tools/spell_checker.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala Fri Apr 10 22:51:18 2020 +0100
@@ -141,9 +141,9 @@
permanent_updates
val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
- val factory_cons = factory_class.getConstructor()
- factory_cons.setAccessible(true)
- val factory = factory_cons.newInstance()
+ val factory_constructor = factory_class.getConstructor()
+ factory_constructor.setAccessible(true)
+ val factory = factory_constructor.newInstance()
val add = Untyped.method(factory_class, "add", classOf[String])
--- a/src/Pure/Tools/update.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Pure/Tools/update.scala Fri Apr 10 22:51:18 2020 +0100
@@ -10,7 +10,7 @@
object Update
{
def update(options: Options, logic: String,
- progress: Progress = No_Progress,
+ progress: Progress = new Progress,
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
--- a/src/Tools/VSCode/src/build_vscode.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala Fri Apr 10 22:51:18 2020 +0100
@@ -17,7 +17,7 @@
/* grammar */
- def build_grammar(options: Options, progress: Progress = No_Progress)
+ def build_grammar(options: Options, progress: Progress = new Progress)
{
val logic = Grammar.default_logic
val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
@@ -30,7 +30,7 @@
/* extension */
- def build_extension(progress: Progress = No_Progress, publish: Boolean = false)
+ def build_extension(progress: Progress = new Progress, publish: Boolean = false)
{
val output_path = extension_dir + Path.explode("out")
progress.echo(output_path.implode)
--- a/src/Tools/VSCode/src/document_model.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Fri Apr 10 22:51:18 2020 +0100
@@ -60,7 +60,7 @@
def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
Document_Model(session, editor, node_name, Content.empty,
- node_required = session.resources.file_formats.is_theory(node_name))
+ node_required = File_Format.registry.is_theory(node_name))
}
sealed case class Document_Model(
--- a/src/Tools/jEdit/src/active.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/active.scala Fri Apr 10 22:51:18 2020 +0100
@@ -8,13 +8,22 @@
import isabelle._
-
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.browser.VFSBrowser
+import org.gjt.sp.jedit.{ServiceManager, View}
object Active
{
+ abstract class Handler
+ {
+ def handle(
+ view: View, text: String, elem: XML.Elem,
+ doc_view: Document_View, snapshot: Document.Snapshot): Boolean
+ }
+
+ def handlers: List[Handler] =
+ ServiceManager.getServiceNames(classOf[Handler]).toList
+ .map(ServiceManager.getService(classOf[Handler], _))
+
def action(view: View, text: String, elem: XML.Elem)
{
GUI_Thread.require {}
@@ -22,72 +31,80 @@
Document_View.get(view.getTextArea) match {
case Some(doc_view) =>
doc_view.rich_text_area.robust_body() {
- val text_area = doc_view.text_area
- val model = doc_view.model
- val buffer = model.buffer
- val snapshot = model.snapshot()
-
+ val snapshot = doc_view.model.snapshot()
if (!snapshot.is_outdated) {
- // FIXME avoid hard-wired stuff
- elem match {
- case XML.Elem(Markup(Markup.BROWSER, _), body) =>
- Isabelle_Thread.fork(name = "browser") {
- val graph_file = Isabelle_System.tmp_file("graph")
- File.write(graph_file, XML.content(body))
- Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
- }
-
- case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
- Isabelle_Thread.fork(name = "graphview") {
- val graph =
- Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
- GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
- }
-
- case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
- GUI_Thread.later {
- val name = Markup.Name.unapply(props) getOrElse ""
- PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
- }
-
- case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
- GUI_Thread.later {
- view.getInputHandler.invokeAction(XML.content(body))
- }
-
- case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
- val link =
- props match {
- case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
- case _ => None
- }
- GUI_Thread.later {
- link.foreach(_.follow(view))
- view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
- }
-
- case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
- if (buffer.isEditable) {
- props match {
- case Position.Id(id) =>
- Isabelle.edit_command(snapshot, text_area,
- props.contains(Markup.PADDING_COMMAND), id, text)
- case _ =>
- if (props.contains(Markup.PADDING_LINE))
- Isabelle.insert_line_padding(text_area, text)
- else text_area.setSelectedText(text)
- }
- text_area.requestFocus
- }
-
- case Protocol.Dialog(id, serial, result) =>
- model.session.dialog_result(id, serial, result)
-
- case _ =>
- }
+ handlers.find(_.handle(view, text, elem, doc_view, snapshot))
}
}
case None =>
}
}
+
+ class Misc_Handler extends Active.Handler
+ {
+ override def handle(
+ view: View, text: String, elem: XML.Elem,
+ doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
+ {
+ val text_area = doc_view.text_area
+ val model = doc_view.model
+ val buffer = model.buffer
+
+ elem match {
+ case XML.Elem(Markup(Markup.BROWSER, _), body) =>
+ Isabelle_Thread.fork(name = "browser") {
+ val graph_file = Isabelle_System.tmp_file("graph")
+ File.write(graph_file, XML.content(body))
+ Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
+ }
+ true
+
+ case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
+ GUI_Thread.later {
+ val name = Markup.Name.unapply(props) getOrElse ""
+ PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
+ }
+ true
+
+ case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
+ GUI_Thread.later {
+ view.getInputHandler.invokeAction(XML.content(body))
+ }
+ true
+
+ case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
+ val link =
+ props match {
+ case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
+ case _ => None
+ }
+ GUI_Thread.later {
+ link.foreach(_.follow(view))
+ view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
+ }
+ true
+
+ case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
+ if (buffer.isEditable) {
+ props match {
+ case Position.Id(id) =>
+ Isabelle.edit_command(snapshot, text_area,
+ props.contains(Markup.PADDING_COMMAND), id, text)
+ case _ =>
+ if (props.contains(Markup.PADDING_LINE))
+ Isabelle.insert_line_padding(text_area, text)
+ else text_area.setSelectedText(text)
+ }
+ text_area.requestFocus
+ }
+ true
+
+ case Protocol.Dialog(id, serial, result) =>
+ model.session.dialog_result(id, serial, result)
+ true
+
+ case _ => false
+ }
+ }
+ }
}
--- a/src/Tools/jEdit/src/document_model.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Apr 10 22:51:18 2020 +0100
@@ -389,7 +389,7 @@
file.foreach(PIDE.plugin.file_watcher.register_parent(_))
val content = Document_Model.File_Content(text)
- val node_required1 = node_required || session.resources.file_formats.is_theory(node_name)
+ val node_required1 = node_required || File_Format.registry.is_theory(node_name)
File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
}
}
@@ -454,7 +454,7 @@
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
if (pending_edits.nonEmpty ||
- !session.resources.file_formats.is_theory(node_name) &&
+ !File_Format.registry.is_theory(node_name) &&
(node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
else {
val text_edits = List(Text.Edit.remove(0, content.text))
--- a/src/Tools/jEdit/src/graphview_dockable.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Fri Apr 10 22:51:18 2020 +0100
@@ -39,14 +39,31 @@
private def reset_implicit(): Unit =
set_implicit(Document.Snapshot.init, no_graph)
- def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
+ class Handler extends Active.Handler
{
- set_implicit(snapshot, graph)
- view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
+ override def handle(
+ view: View, text: String, elem: XML.Elem,
+ doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
+ {
+ elem match {
+ case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
+ Isabelle_Thread.fork(name = "graphview") {
+ val graph =
+ Exn.capture {
+ Graph_Display.decode_graph(body).transitive_reduction_acyclic
+ }
+ GUI_Thread.later {
+ set_implicit(snapshot, graph)
+ view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")
+ }
+ }
+ true
+ case _ => false
+ }
+ }
}
}
-
class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val snapshot = Graphview_Dockable.implicit_snapshot
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Apr 10 22:51:18 2020 +0100
@@ -126,7 +126,7 @@
session_requirements = logic_requirements)
def session_build(
- options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
+ options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int =
{
Build.build(session_options(options), progress = progress, build_heap = true,
no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
--- a/src/Tools/jEdit/src/plugin.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Apr 10 22:51:18 2020 +0100
@@ -289,10 +289,10 @@
@volatile private var startup_failure: Option[Throwable] = None
@volatile private var startup_notified = false
- private def init_view(view: View)
+ private def init_editor(view: View)
{
+ Keymap_Merge.check_dialog(view)
Session_Build.check_dialog(view)
- Keymap_Merge.check_dialog(view)
}
private def init_title(view: View)
@@ -341,7 +341,7 @@
jEdit.propertiesChanged()
val view = jEdit.getActiveView()
- init_view(view)
+ init_editor(view)
PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
@@ -480,7 +480,7 @@
shutting_down.change(_ => false)
val view = jEdit.getActiveView()
- if (view != null) init_view(view)
+ if (view != null) init_editor(view)
}
override def stop()
--- a/src/Tools/jEdit/src/services.xml Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/services.xml Fri Apr 10 22:51:18 2020 +0100
@@ -44,4 +44,10 @@
<SERVICE CLASS="console.Shell" NAME="Scala">
new isabelle.jedit.Scala_Console();
</SERVICE>
+ <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="misc">
+ new isabelle.jedit.Active$Misc_Handler();
+ </SERVICE>
+ <SERVICE CLASS="isabelle.jedit.Active$Handler" NAME="graphview">
+ new isabelle.jedit.Graphview_Dockable$Handler()
+ </SERVICE>
</SERVICES>
--- a/src/Tools/jEdit/src/session_build.scala Fri Apr 10 22:50:59 2020 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Fri Apr 10 22:51:18 2020 +0100
@@ -23,18 +23,18 @@
{
def check_dialog(view: View)
{
- GUI_Thread.require {}
-
val options = PIDE.options.value
- try {
- if (JEdit_Sessions.session_no_build ||
+ Isabelle_Thread.fork() {
+ try {
+ if (JEdit_Sessions.session_no_build ||
JEdit_Sessions.session_build(options, no_build = true) == 0)
- JEdit_Sessions.session_start(options)
- else new Dialog(view)
- }
- catch {
- case exn: Throwable =>
- GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ JEdit_Sessions.session_start(options)
+ else GUI_Thread.later { new Dialog(view) }
+ }
+ catch {
+ case exn: Throwable =>
+ GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ }
}
}
@@ -57,8 +57,6 @@
/* progress */
- @volatile private var is_stopped = false
-
private val progress = new Progress {
override def echo(txt: String): Unit =
GUI_Thread.later {
@@ -68,8 +66,6 @@
}
override def theory(theory: Progress.Theory): Unit = echo(theory.message)
-
- override def stopped: Boolean = is_stopped
}
@@ -132,7 +128,7 @@
private def stopping()
{
- is_stopped = true
+ progress.stop
set_actions(new Label("Stopping ..."))
}