--- a/src/Pure/PIDE/document.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Pure/PIDE/document.scala Mon Jun 26 23:12:43 2017 +0200
@@ -123,6 +123,7 @@
override def toString: String = if (is_theory) theory else node
def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
+ def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
}
--- a/src/Pure/PIDE/xml.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Pure/PIDE/xml.scala Mon Jun 26 23:12:43 2017 +0200
@@ -35,6 +35,7 @@
}
case class Text(content: String) extends Tree
+ def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
--- a/src/Pure/Pure.thy Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Pure/Pure.thy Mon Jun 26 23:12:43 2017 +0200
@@ -7,11 +7,11 @@
theory Pure
keywords
"!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
- "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
- "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
+ "\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+ "overloaded" "pervasive" "premises" "structure" "unchecked"
and "private" "qualified" :: before_command
- and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
- "obtains" "shows" "where" "|" :: quasi_command
+ and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
+ "obtains" "shows" "when" "where" "|" :: quasi_command
and "text" "txt" :: document_body
and "text_raw" :: document_raw
and "default_sort" :: thy_decl
--- a/src/Pure/Thy/html.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Pure/Thy/html.scala Mon Jun 26 23:12:43 2017 +0200
@@ -224,6 +224,61 @@
HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
+ /* GUI elements */
+
+ object GUI
+ {
+ private def optional_value(text: String): XML.Attributes =
+ proper_string(text).map(a => "value" -> a).toList
+
+ private def optional_name(name: String): XML.Attributes =
+ proper_string(name).map(a => "name" -> a).toList
+
+ private def optional_title(tooltip: String): XML.Attributes =
+ proper_string(tooltip).map(a => "title" -> a).toList
+
+ private def optional_submit(submit: Boolean): XML.Attributes =
+ if (submit) List("onChange" -> "this.form.submit()") else Nil
+
+ private def optional_checked(selected: Boolean): XML.Attributes =
+ if (selected) List("checked" -> "") else Nil
+
+ private def optional_action(action: String): XML.Attributes =
+ proper_string(action).map(a => "action" -> a).toList
+
+ def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false)
+ : XML.Elem =
+ XML.Elem(
+ Markup("button",
+ List("type" -> (if (submit) "submit" else "button"), "value" -> "true") :::
+ optional_name(name) ::: optional_title(tooltip)), body)
+
+ def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
+ selected: Boolean = false): XML.Elem =
+ XML.elem("label",
+ XML.elem(
+ Markup("input",
+ List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) :::
+ optional_title(tooltip) ::: optional_submit(submit) :::
+ optional_checked(selected))) :: body)
+
+ def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "",
+ submit: Boolean = false): XML.Elem =
+ XML.elem(Markup("input",
+ List("type" -> "text") :::
+ (if (columns > 0) List("size" -> columns.toString) else Nil) :::
+ optional_value(text) ::: optional_name(name) :::
+ optional_title(tooltip) ::: optional_submit(submit)))
+
+ def parameter(text: String = "", name: String = ""): XML.Elem =
+ XML.elem(
+ Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name)))
+
+ def form(body: XML.Body, name: String = "", action: String = ""): XML.Elem =
+ XML.Elem(Markup("form", optional_name(name) ::: optional_action(action)), body)
+ }
+
+
/* document */
val header: String =
--- a/src/Pure/Thy/sessions.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Jun 26 23:12:43 2017 +0200
@@ -81,8 +81,11 @@
theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))),
files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_)))))
- def get_file(file: JFile): Option[Document.Node.Name] =
- files.getOrElse(file.getCanonicalFile, Nil).headOption
+ def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
+ {
+ val res = files.getOrElse(file.getCanonicalFile, Nil).headOption
+ if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res
+ }
}
object Base
--- a/src/Pure/Thy/thy_header.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala Mon Jun 26 23:12:43 2017 +0200
@@ -89,8 +89,7 @@
def theory_name(s: String): String =
s match {
- case Thy_File_Name(name) =>
- bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
+ case Thy_File_Name(name) => bootstrap_name(name)
case Import_Name(name) =>
ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
case _ => ""
@@ -102,6 +101,9 @@
def is_bootstrap(theory: String): Boolean =
bootstrap_thys.exists({ case (_, b) => b == theory })
+ def bootstrap_name(theory: String): String =
+ bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
+
/* header */
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Jun 26 23:12:43 2017 +0200
@@ -91,7 +91,7 @@
def node_file(name: Document.Node.Name): JFile = new JFile(name.node)
def node_name(file: JFile): Document.Node.Name =
- session_base.known.get_file(file) getOrElse {
+ session_base.known.get_file(file, bootstrap = true) getOrElse {
val node = file.getPath
theory_name(Sessions.DRAFT, Thy_Header.theory_name(node)) match {
case (true, theory) => Document.Node.Name.loaded_theory(theory)
--- a/src/Tools/jEdit/src/jedit_resources.scala Mon Jun 26 16:59:44 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Mon Jun 26 23:12:43 2017 +0200
@@ -26,7 +26,7 @@
/* document node name */
def known_file(path: String): Option[Document.Node.Name] =
- JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_))
+ JEdit_Lib.check_file(path).flatMap(session_base.known.get_file(_, bootstrap = true))
def node_name(path: String): Document.Node.Name =
known_file(path) getOrElse {