71 type Options = List[(String, Option[String])] |
71 type Options = List[(String, Option[String])] |
72 |
72 |
73 case class Session_Info( |
73 case class Session_Info( |
74 dir: Path, |
74 dir: Path, |
75 name: String, |
75 name: String, |
76 path: String, |
76 reset_name: Boolean, |
77 parent: String, |
77 parent: String, |
78 alt_name: Option[String], |
|
79 description: String, |
78 description: String, |
80 options: Options, |
79 options: Options, |
81 theories: List[(Options, String)], |
80 theories: List[(Options, String)], |
82 files: List[String]) |
81 files: List[String]) |
83 |
82 |
84 private object Parser extends Parse.Parser |
83 private object Parser extends Parse.Parser |
85 { |
84 { |
86 val SESSION = "session" |
85 val SESSION = "session" |
87 val IN = "in" |
86 val IN = "in" |
88 val NAME = "name" |
|
89 val DESCRIPTION = "description" |
87 val DESCRIPTION = "description" |
90 val OPTIONS = "options" |
88 val OPTIONS = "options" |
91 val THEORIES = "theories" |
89 val THEORIES = "theories" |
92 val FILES = "files" |
90 val FILES = "files" |
93 |
91 |
94 val syntax = |
92 val syntax = |
95 Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + |
93 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" + |
96 SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES |
94 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES |
97 |
95 |
98 def session_info(dir: Path): Parser[Session_Info] = |
96 def session_info(dir: Path): Parser[Session_Info] = |
99 { |
97 { |
100 val session_name = atom("session name", _.is_name) |
98 val session_name = atom("session name", _.is_name) |
101 val theory_name = atom("theory name", _.is_name) |
99 val theory_name = atom("theory name", _.is_name) |
102 val file_name = atom("file name", _.is_name) |
|
103 |
100 |
104 val option = |
101 val option = |
105 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } |
102 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } |
106 val options: Parser[Options] = |
103 val options: Parser[Options] = |
107 keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]") |
104 keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]") |
109 val theories = |
106 val theories = |
110 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^ |
107 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^ |
111 { case _ ~ (x ~ y) => (x, y) } |
108 { case _ ~ (x ~ y) => (x, y) } |
112 |
109 |
113 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ |
110 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~ |
114 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~ |
111 (keyword("!") ^^^ true | success(false)) ~ |
|
112 (opt(keyword(IN) ~! string ^^ { case _ ~ x => Path.explode(x) })) ~ |
115 (keyword("=") ~> session_name <~ keyword("+")) ~ |
113 (keyword("=") ~> session_name <~ keyword("+")) ~ |
116 (opt(keyword(NAME) ~! session_name ^^ { case _ ~ x => x })) ~ |
|
117 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~ |
114 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~ |
118 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~ |
115 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~ |
119 rep(theories) ~ |
116 rep(theories) ~ |
120 (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^ |
117 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^ |
121 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => |
118 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => |
122 Session_Info(dir, a, b getOrElse a, c, d, e, f, |
119 val dir1 = dir + c.getOrElse(Path.basic(a)) |
123 g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) } |
120 val thys = g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten |
|
121 Session_Info(dir1, a, b, d, e, f, thys, h) } |
124 } |
122 } |
125 |
123 |
126 def parse_entries(dir: Path, root: File): List[Session_Info] = |
124 def parse_entries(dir: Path, root: File): List[Session_Info] = |
127 { |
125 { |
128 val toks = syntax.scan(Standard_System.read_file(root)) |
126 val toks = syntax.scan(Standard_System.read_file(root)) |