src/Tools/jEdit/src/document_model.scala
changeset 73774 c42144d9dde6
parent 73665 56c0a793cd8b
child 73959 7202e12cb324
equal deleted inserted replaced
73772:d3f2038198ae 73774:c42144d9dde6
   328               PIDE.resources, snapshot, html_context, Presentation.elements2,
   328               PIDE.resources, snapshot, html_context, Presentation.elements2,
   329               plain_text = query.startsWith(plain_text_prefix))
   329               plain_text = query.startsWith(plain_text_prefix))
   330           HTTP.Response.html(document.content)
   330           HTTP.Response.html(document.content)
   331         })
   331         })
   332 
   332 
   333     List(HTTP.fonts(fonts_root), html)
   333     List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), html)
   334   }
   334   }
   335 }
   335 }
   336 
   336 
   337 sealed abstract class Document_Model extends Document.Model
   337 sealed abstract class Document_Model extends Document.Model
   338 {
   338 {