src/Pure/Thy/sessions.scala
changeset 66818 5bc903a60932
parent 66780 bf54ca580bf2
child 66819 064c80e9d1cf
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 08 16:50:37 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 09 16:43:15 2017 +0200
     1.3 @@ -550,26 +550,26 @@
     1.4        (THEORIES, Keyword.QUASI_COMMAND) +
     1.5        (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
     1.6  
     1.7 +  abstract class Entry
     1.8 +  sealed case class Chapter(name: String) extends Entry
     1.9 +  sealed case class Session_Entry(
    1.10 +    pos: Position.T,
    1.11 +    name: String,
    1.12 +    groups: List[String],
    1.13 +    path: String,
    1.14 +    parent: Option[String],
    1.15 +    description: String,
    1.16 +    options: List[Options.Spec],
    1.17 +    imports: List[String],
    1.18 +    theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    1.19 +    document_files: List[(String, String)]) extends Entry
    1.20 +  {
    1.21 +    def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    1.22 +      theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    1.23 +  }
    1.24 +
    1.25    private object Parser extends Parse.Parser with Options.Parser
    1.26    {
    1.27 -    private abstract class Entry
    1.28 -    private sealed case class Chapter(name: String) extends Entry
    1.29 -    private sealed case class Session_Entry(
    1.30 -      pos: Position.T,
    1.31 -      name: String,
    1.32 -      groups: List[String],
    1.33 -      path: String,
    1.34 -      parent: Option[String],
    1.35 -      description: String,
    1.36 -      options: List[Options.Spec],
    1.37 -      imports: List[String],
    1.38 -      theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
    1.39 -      document_files: List[(String, String)]) extends Entry
    1.40 -    {
    1.41 -      def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] =
    1.42 -        theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) })
    1.43 -    }
    1.44 -
    1.45      private val chapter: Parser[Chapter] =
    1.46      {
    1.47        val chapter_name = atom("chapter name", _.is_name)
    1.48 @@ -618,70 +618,85 @@
    1.49              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    1.50      }
    1.51  
    1.52 -    def parse_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
    1.53 +    def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
    1.54      {
    1.55 -      def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
    1.56 -      {
    1.57 -        try {
    1.58 -          val name = entry.name
    1.59 -
    1.60 -          if (name == "" || name == DRAFT) error("Bad session name")
    1.61 -          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    1.62 -          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    1.63 -
    1.64 -          val session_options = options ++ entry.options
    1.65 -
    1.66 -          val theories =
    1.67 -            entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
    1.68 -
    1.69 -          val global_theories =
    1.70 -            for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
    1.71 -            yield {
    1.72 -              val thy_name = Path.explode(thy).expand.base_name
    1.73 -              if (Long_Name.is_qualified(thy_name))
    1.74 -                error("Bad qualified name for global theory " +
    1.75 -                  quote(thy_name) + Position.here(pos))
    1.76 -              else thy_name
    1.77 -            }
    1.78 -
    1.79 -          val document_files =
    1.80 -            entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
    1.81 -
    1.82 -          val meta_digest =
    1.83 -            SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
    1.84 -              entry.theories_no_position, entry.document_files).toString)
    1.85 -
    1.86 -          val info =
    1.87 -            Info(name, entry_chapter, select, entry.pos, entry.groups,
    1.88 -              path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
    1.89 -              entry.imports, theories, global_theories, document_files, meta_digest)
    1.90 -
    1.91 -          (name, info)
    1.92 -        }
    1.93 -        catch {
    1.94 -          case ERROR(msg) =>
    1.95 -            error(msg + "\nThe error(s) above occurred in session entry " +
    1.96 -              quote(entry.name) + Position.here(entry.pos))
    1.97 -        }
    1.98 -      }
    1.99 -
   1.100        val toks = Token.explode(root_syntax.keywords, File.read(path))
   1.101        val start = Token.Pos.file(path.implode)
   1.102  
   1.103        parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
   1.104 -        case Success(result, _) =>
   1.105 -          var entry_chapter = "Unsorted"
   1.106 -          val infos = new mutable.ListBuffer[(String, Info)]
   1.107 -          result.foreach {
   1.108 -            case Chapter(name) => entry_chapter = name
   1.109 -            case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   1.110 -          }
   1.111 -          infos.toList
   1.112 +        case Success(result, _) => result
   1.113          case bad => error(bad.toString)
   1.114        }
   1.115      }
   1.116    }
   1.117  
   1.118 +  def parse_root(options: Options, select: Boolean, path: Path): List[Entry] =
   1.119 +    Parser.parse_root(options, select, path)
   1.120 +
   1.121 +  def read_root(options: Options, select: Boolean, path: Path): List[(String, Info)] =
   1.122 +  {
   1.123 +    def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
   1.124 +    {
   1.125 +      try {
   1.126 +        val name = entry.name
   1.127 +
   1.128 +        if (name == "" || name == DRAFT) error("Bad session name")
   1.129 +        if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
   1.130 +        if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
   1.131 +
   1.132 +        val session_options = options ++ entry.options
   1.133 +
   1.134 +        val theories =
   1.135 +          entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
   1.136 +
   1.137 +        val global_theories =
   1.138 +          for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
   1.139 +          yield {
   1.140 +            val thy_name = Path.explode(thy).expand.base_name
   1.141 +            if (Long_Name.is_qualified(thy_name))
   1.142 +              error("Bad qualified name for global theory " +
   1.143 +                quote(thy_name) + Position.here(pos))
   1.144 +            else thy_name
   1.145 +          }
   1.146 +
   1.147 +        val document_files =
   1.148 +          entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
   1.149 +
   1.150 +        val meta_digest =
   1.151 +          SHA1.digest((entry_chapter, name, entry.parent, entry.options, entry.imports,
   1.152 +            entry.theories_no_position, entry.document_files).toString)
   1.153 +
   1.154 +        val info =
   1.155 +          Info(name, entry_chapter, select, entry.pos, entry.groups,
   1.156 +            path.dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
   1.157 +            entry.imports, theories, global_theories, document_files, meta_digest)
   1.158 +
   1.159 +        (name, info)
   1.160 +      }
   1.161 +      catch {
   1.162 +        case ERROR(msg) =>
   1.163 +          error(msg + "\nThe error(s) above occurred in session entry " +
   1.164 +            quote(entry.name) + Position.here(entry.pos))
   1.165 +      }
   1.166 +    }
   1.167 +
   1.168 +    var entry_chapter = "Unsorted"
   1.169 +    val infos = new mutable.ListBuffer[(String, Info)]
   1.170 +    parse_root(options, select, path).foreach {
   1.171 +      case Chapter(name) => entry_chapter = name
   1.172 +      case entry: Session_Entry => infos += make_info(entry_chapter, entry)
   1.173 +    }
   1.174 +    infos.toList
   1.175 +  }
   1.176 +
   1.177 +  def parse_roots(roots: Path): List[String] =
   1.178 +  {
   1.179 +    for {
   1.180 +      line <- split_lines(File.read(roots))
   1.181 +      if !(line == "" || line.startsWith("#"))
   1.182 +    } yield line
   1.183 +  }
   1.184 +
   1.185  
   1.186    /* load sessions from certain directories */
   1.187  
   1.188 @@ -714,10 +729,9 @@
   1.189        val roots = dir + ROOTS
   1.190        if (roots.is_file) {
   1.191          for {
   1.192 -          line <- split_lines(File.read(roots))
   1.193 -          if !(line == "" || line.startsWith("#"))
   1.194 +          entry <- parse_roots(roots)
   1.195            dir1 =
   1.196 -            try { check_session_dir(dir + Path.explode(line)) }
   1.197 +            try { check_session_dir(dir + Path.explode(entry)) }
   1.198              catch {
   1.199                case ERROR(msg) =>
   1.200                  error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   1.201 @@ -743,7 +757,7 @@
   1.202          }
   1.203        }).toList.map(_._2)
   1.204  
   1.205 -    make(unique_roots.flatMap(p => Parser.parse_root(options, p._1, p._2)))
   1.206 +    make(unique_roots.flatMap(p => read_root(options, p._1, p._2)))
   1.207    }
   1.208  
   1.209