# HG changeset patch
# User wenzelm
# Date 1503336002 -7200
# Node ID 5c0a3f63057dc3bd8802dfbaf3b3aeea55241216
# Parent  439296f00ab535084b57abcf5d169e340511243a
proper argument type (amending 8d5cb4ea2b7c);

diff -r 439296f00ab5 -r 5c0a3f63057d src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Aug 21 17:35:59 2017 +0200
+++ b/src/Pure/General/http.scala	Mon Aug 21 19:20:02 2017 +0200
@@ -141,8 +141,8 @@
   /* welcome */
 
   val welcome: Handler =
-    get("/", uri =>
-      if (uri.toString == "/") {
+    get("/", arg =>
+      if (arg.uri.toString == "/") {
         val id =
           Isabelle_System.getenv("ISABELLE_ID") match {
             case "" => Mercurial.repository(Path.explode("~~")).id()
@@ -160,9 +160,9 @@
       Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
 
   def fonts(root: String = "/fonts"): Handler =
-    get(root, uri =>
+    get(root, arg =>
       {
-        val uri_name = uri.toString
+        val uri_name = arg.uri.toString
         if (uri_name == root) Some(Response.text(cat_lines(html_fonts.map(_._1))))
         else html_fonts.collectFirst({ case (a, b) if uri_name == root + "/" + a => Response(b) })
       })