src/Pure/General/http.scala
changeset 73774 c42144d9dde6
parent 73692 3696bb4085ed
child 73779 2cd23d587db9
equal deleted inserted replaced
73772:d3f2038198ae 73774:c42144d9dde6
   269 
   269 
   270 
   270 
   271   /** Isabelle resources **/
   271   /** Isabelle resources **/
   272 
   272 
   273   lazy val isabelle_resources: List[Handler] =
   273   lazy val isabelle_resources: List[Handler] =
   274     List(welcome, fonts())
   274     List(welcome(), fonts())
   275 
   275 
   276 
   276 
   277   /* welcome */
   277   /* welcome */
   278 
   278 
   279   val welcome: Handler =
   279   def welcome(root: String = "/"): Handler =
   280     Handler.get("/", arg =>
   280     Handler.get(root, arg =>
   281       if (arg.uri.toString == "/") {
   281       if (arg.uri.toString == root) {
   282         val id = Isabelle_System.isabelle_id()
   282         val id = Isabelle_System.isabelle_id()
   283         Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
   283         Some(Response.text("Welcome to Isabelle/" + id + ": " + Distribution.version))
   284       }
   284       }
   285       else None)
   285       else None)
   286 
   286