src/Pure/Thy/present.scala
changeset 65089 1d219d76873b
parent 65083 9a0e34edfad1
child 65344 b99283eed13c
equal deleted inserted replaced
65088:18f2d388fab4 65089:1d219d76873b
    98     graph_file: JFile,
    98     graph_file: JFile,
    99     info: Sessions.Info,
    99     info: Sessions.Info,
   100     name: String)
   100     name: String)
   101   {
   101   {
   102     val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
   102     val session_prefix = browser_info + Path.basic(info.chapter) + Path.basic(name)
       
   103     val session_fonts = session_prefix + Path.explode("fonts")
   103 
   104 
   104     if (info.options.bool("browser_info")) {
   105     if (info.options.bool("browser_info")) {
   105       Isabelle_System.mkdirs(session_prefix)
   106       Isabelle_System.mkdirs(session_fonts)
   106 
   107 
   107       val session_graph = session_prefix + Path.basic("session_graph.pdf")
   108       val session_graph = session_prefix + Path.basic("session_graph.pdf")
   108       File.copy(graph_file, session_graph.file)
   109       File.copy(graph_file, session_graph.file)
   109       Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
   110       Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
   110 
   111 
   111       File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
   112       File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
   112 
   113 
   113       for (font <- Isabelle_System.fonts(html = true))
   114       for (font <- Isabelle_System.fonts(html = true))
   114         File.copy(font, session_prefix)
   115         File.copy(font, session_fonts)
   115     }
   116     }
   116   }
   117   }
   117 }
   118 }