# HG changeset patch
# User wenzelm
# Date 1498511563 -7200
# Node ID c8604c9f3a8ae66d2ee98d4a33df475d368ee34c
# Parent  6e6eeef63589f07b793fd9e9d3ba95b1dac7ed5d# Parent  31c9b09cc1d4b1f922279684c04ebce4711af974
merged

diff -r 6e6eeef63589 -r c8604c9f3a8a src/Pure/PIDE/document.scala
--- 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))
     }
 
 
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Pure/PIDE/xml.scala
--- 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)
 
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Pure/Pure.thy
--- 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
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Pure/Thy/html.scala
--- 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 =
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Pure/Thy/sessions.scala
--- 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
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Pure/Thy/thy_header.scala
--- 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 */
 
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Tools/VSCode/src/vscode_resources.scala
--- 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)
diff -r 6e6eeef63589 -r c8604c9f3a8a src/Tools/jEdit/src/jedit_resources.scala
--- 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 {