# HG changeset patch
# User wenzelm
# Date 1488461833 -3600
# Node ID c20905a5bc8e78021aed5760d30794ba82bce6e4
# Parent  2b6ed26b7597e147c0fd9902e706b810be9756a1
handler for Isabelle version;

diff -r 2b6ed26b7597 -r c20905a5bc8e src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Mar 02 14:14:48 2017 +0100
+++ b/src/Pure/General/http.scala	Thu Mar 02 14:37:13 2017 +0100
@@ -15,6 +15,8 @@
 
 object HTTP
 {
+  /** server **/
+
   /* response */
 
   object Response
@@ -92,7 +94,7 @@
     override def toString: String = url
   }
 
-  def server(handlers: Handler*): Server =
+  def server(handlers: List[Handler] = isabelle_resources): Server =
   {
     val localhost = InetAddress.getByName("127.0.0.1")
     val http_server = HttpServer.create(new InetSocketAddress(localhost, 0), 0)
@@ -104,7 +106,29 @@
   }
 
 
-  /* Isabelle resources */
+
+  /** Isabelle resources **/
+
+  lazy val isabelle_resources: List[Handler] =
+    List(welcome(), fonts())
+
+
+  /* welcome */
+
+  def welcome(root: String = "/"): Handler =
+    get(root, uri =>
+      if (uri.toString == "/") {
+        val id =
+          Isabelle_System.getenv("ISABELLE_ID") match {
+            case "" => Mercurial.repository(Path.explode("~~")).id()
+            case id => id
+          }
+        Some(Response.text("Welcome to Isabelle (" + id + ")"))
+      }
+      else None)
+
+
+  /* fonts */
 
   private lazy val isabelle_fonts: SortedMap[String, Bytes] =
     SortedMap(