src/Pure/Thy/present.scala
author wenzelm
Wed Apr 15 15:27:45 2015 +0200 (2015-04-15)
changeset 60077 55cb9462e602
parent 51987 7d8e0e3c553b
child 61372 cf40b6b1de54
permissions -rw-r--r--
tuned signature, clarified modules;
wenzelm@50707
     1
/*  Title:      Pure/Thy/present.scala
wenzelm@50707
     2
    Author:     Makarius
wenzelm@50707
     3
wenzelm@50707
     4
Theory presentation: HTML.
wenzelm@50707
     5
*/
wenzelm@50707
     6
wenzelm@50707
     7
package isabelle
wenzelm@50707
     8
wenzelm@50707
     9
wenzelm@51402
    10
import scala.collection.immutable.SortedMap
wenzelm@51402
    11
wenzelm@51402
    12
wenzelm@50707
    13
object Present
wenzelm@50707
    14
{
wenzelm@60077
    15
  /* session graph */
wenzelm@60077
    16
wenzelm@60077
    17
  def session_graph(
wenzelm@60077
    18
    parent_session: String,
wenzelm@60077
    19
    parent_loaded: String => Boolean,
wenzelm@60077
    20
    deps: List[Thy_Info.Dep]): Graph_Display.Graph =
wenzelm@60077
    21
  {
wenzelm@60077
    22
    val parent_session_node =
wenzelm@60077
    23
      Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
wenzelm@60077
    24
wenzelm@60077
    25
    def node(name: Document.Node.Name): Graph_Display.Node =
wenzelm@60077
    26
      if (parent_loaded(name.theory)) parent_session_node
wenzelm@60077
    27
      else Graph_Display.Node(name.theory, "theory." + name.theory)
wenzelm@60077
    28
wenzelm@60077
    29
    (Graph_Display.empty_graph /: deps) {
wenzelm@60077
    30
      case (g, dep) =>
wenzelm@60077
    31
        if (parent_loaded(dep.name.theory)) g
wenzelm@60077
    32
        else {
wenzelm@60077
    33
          val a = node(dep.name)
wenzelm@60077
    34
          val bs = dep.header.imports.map({ case (name, _) => node(name) })
wenzelm@60077
    35
          ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a))
wenzelm@60077
    36
        }
wenzelm@60077
    37
    }
wenzelm@60077
    38
  }
wenzelm@60077
    39
wenzelm@60077
    40
wenzelm@51399
    41
  /* maintain chapter index -- NOT thread-safe */
wenzelm@50707
    42
wenzelm@50707
    43
  private val index_path = Path.basic("index.html")
wenzelm@51399
    44
  private val sessions_path = Path.basic(".sessions")
wenzelm@50707
    45
wenzelm@51402
    46
  private def read_sessions(dir: Path): List[(String, String)] =
wenzelm@51402
    47
  {
wenzelm@51416
    48
    val path = dir + sessions_path
wenzelm@51416
    49
    if (path.is_file) {
wenzelm@51416
    50
      import XML.Decode._
wenzelm@51416
    51
      list(pair(string, string))(YXML.parse_body(File.read(path)))
wenzelm@51416
    52
    }
wenzelm@51416
    53
    else Nil
wenzelm@51402
    54
  }
wenzelm@50707
    55
wenzelm@51402
    56
  private def write_sessions(dir: Path, sessions: List[(String, String)])
wenzelm@51402
    57
  {
wenzelm@51402
    58
    import XML.Encode._
wenzelm@51402
    59
    File.write(dir + sessions_path, YXML.string_of_body(list(pair(string, string))(sessions)))
wenzelm@51402
    60
  }
wenzelm@50707
    61
wenzelm@51402
    62
  def update_chapter_index(info_path: Path, chapter: String, new_sessions: List[(String, String)])
wenzelm@51399
    63
  {
wenzelm@51399
    64
    val dir = info_path + Path.basic(chapter)
wenzelm@51399
    65
    Isabelle_System.mkdirs(dir)
wenzelm@50707
    66
wenzelm@51399
    67
    val sessions0 =
wenzelm@51406
    68
      try { read_sessions(dir) }
wenzelm@51987
    69
      catch { case _: XML.Error => Nil }
wenzelm@51399
    70
wenzelm@51402
    71
    val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList
wenzelm@51402
    72
wenzelm@51399
    73
    write_sessions(dir, sessions)
wenzelm@51399
    74
    File.write(dir + index_path, HTML.chapter_index(chapter, sessions))
wenzelm@51399
    75
  }
wenzelm@50707
    76
}