equal
deleted
inserted
replaced
428 /* HTTP server */ |
428 /* HTTP server */ |
429 |
429 |
430 val http_root: String = "/" + UUID.random().toString |
430 val http_root: String = "/" + UUID.random().toString |
431 |
431 |
432 val http_server: HTTP.Server = |
432 val http_server: HTTP.Server = |
433 HTTP.server(services = Document_Model.preview_service :: HTTP.isabelle_services) |
433 HTTP.server(services = Document_Model.Preview :: HTTP.isabelle_services) |
434 |
434 |
435 |
435 |
436 /* start and stop */ |
436 /* start and stop */ |
437 |
437 |
438 private val shutting_down = Synchronized(false) |
438 private val shutting_down = Synchronized(false) |