src/Pure/Tools/build.scala
changeset 64855 8fcc23e8e1d9
parent 64854 f5aa712e6250
child 64856 5e9bf964510a
equal deleted inserted replaced
64854:f5aa712e6250 64855:8fcc23e8e1d9
    95 
    95 
    96   /* source dependencies and static content */
    96   /* source dependencies and static content */
    97 
    97 
    98   object Session_Content
    98   object Session_Content
    99   {
    99   {
   100     def empty: Session_Content =
   100     val empty: Session_Content =
   101       Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
   101       Session_Content(Set.empty, Map.empty, Nil, Outer_Syntax.empty,
   102         Nil, Graph_Display.empty_graph)
   102         Nil, Graph_Display.empty_graph)
   103 
   103 
   104     def bootstrap: Session_Content =
   104     lazy val bootstrap: Session_Content =
   105       Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
   105       Session_Content(Set.empty, Map.empty, Thy_Header.bootstrap_header,
   106         Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
   106         Thy_Header.bootstrap_syntax, Nil, Graph_Display.empty_graph)
   107   }
   107   }
   108 
   108 
   109   sealed case class Session_Content(
   109   sealed case class Session_Content(