1 /* Title: Pure/ML/ml_root.scala |
|
2 Author: Makarius |
|
3 |
|
4 Support for ML project ROOT file, with imitation of ML "use" commands. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object ML_Root |
|
11 { |
|
12 /* parser */ |
|
13 |
|
14 val USE = "use" |
|
15 val USE_DEBUG = "use_debug" |
|
16 val USE_NO_DEBUG = "use_no_debug" |
|
17 val USE_THY = "use_thy" |
|
18 |
|
19 lazy val syntax = |
|
20 Outer_Syntax.init() + ";" + |
|
21 (USE, Some((Keyword.THY_LOAD, Nil)), None) + |
|
22 (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) + |
|
23 (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) + |
|
24 (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None) |
|
25 |
|
26 private object Parser extends Parse.Parser |
|
27 { |
|
28 val entry: Parser[Path] = |
|
29 command(USE_THY) ~! string ^^ |
|
30 { case _ ~ a => Resources.thy_path(Path.explode(a)) } | |
|
31 (command(USE) | command(USE_DEBUG) | command(USE_NO_DEBUG)) ~! string ^^ |
|
32 { case _ ~ a => Path.explode(a) } |
|
33 |
|
34 val entries: Parser[List[Path]] = |
|
35 rep(entry <~ $$$(";")) |
|
36 } |
|
37 |
|
38 def read_files(root: Path): List[Path] = |
|
39 { |
|
40 val toks = Token.explode(syntax.keywords, File.read(root)) |
|
41 val start = Token.Pos.file(root.implode) |
|
42 |
|
43 Parser.parse_all(Parser.entries, Token.reader(toks, start)) match { |
|
44 case Parser.Success(entries, _) => entries |
|
45 case bad => error(bad.toString) |
|
46 } |
|
47 } |
|
48 } |
|