--- a/NEWS Mon Mar 23 13:26:35 2020 +0100
+++ b/NEWS Thu Mar 26 11:48:52 2020 +0100
@@ -222,6 +222,9 @@
* Isabelle/Scala support for proof terms (with full type/term
information) in module isabelle.Term.
+* Isabelle/Scala: more scalable output of YXML files, e.g. relevant for
+"isabelle dump".
+
* Theory export via Isabelle/Scala has been reworked. The former "fact"
name space is now split into individual "thm" items: names are
potentially indexed, such as "foo" for singleton facts, or "bar(1)",
--- a/src/Pure/Thy/export_theory.ML Mon Mar 23 13:26:35 2020 +0100
+++ b/src/Pure/Thy/export_theory.ML Thu Mar 26 11:48:52 2020 +0100
@@ -251,7 +251,7 @@
(* theorems and proof terms *)
val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
- val prep_thm = clean_thm #> Thm.unconstrainT;
+ val prep_thm = clean_thm #> Thm.unconstrainT #> Thm.strip_shyps;
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
--- a/src/Pure/Tools/dump.scala Mon Mar 23 13:26:35 2020 +0100
+++ b/src/Pure/Tools/dump.scala Thu Mar 26 11:48:52 2020 +0100
@@ -481,6 +481,10 @@
val progress = new Console_Progress(verbose = verbose)
+ val start_date = Date.now()
+
+ if (verbose) progress.echo("Started at " + Build_Log.print_date(start_date))
+
progress.interrupt_handler {
dump(options, logic,
aspects = aspects,
@@ -497,5 +501,11 @@
session_groups = session_groups,
sessions = sessions))
}
+
+ val end_date = Date.now()
+ val timing = end_date.time - start_date.time
+
+ if (verbose) progress.echo("\nFinished at " + Build_Log.print_date(end_date))
+ progress.echo(timing.message_hms + " elapsed time")
})
}