--- a/src/Pure/PIDE/protocol.scala Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Nov 23 15:14:58 2020 +0100
@@ -21,6 +21,21 @@
val Error_Message_Marker = Protocol_Message.Marker("error_message")
+ /* batch build */
+
+ object Loading_Theory
+ {
+ def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
+ (props, props, props) match {
+ case (Markup.Name(name), Position.File(file), Position.Id(id))
+ if Path.is_wellformed(file) =>
+ val master_dir = Path.explode(file).dir.implode
+ Some((Document.Node.Name(file, master_dir, name), id))
+ case _ => None
+ }
+ }
+
+
/* document editing */
object Commands_Accepted
@@ -188,13 +203,13 @@
object Export
{
sealed case class Args(
- id: Option[String],
- serial: Long,
+ id: Option[String] = None,
+ serial: Long = 0L,
theory_name: String,
name: String,
- executable: Boolean,
- compress: Boolean,
- strict: Boolean)
+ executable: Boolean = false,
+ compress: Boolean = true,
+ strict: Boolean = true)
{
def compound_name: String = isabelle.Export.compound_name(theory_name, name)
}