equal
deleted
inserted
replaced
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 |