equal
deleted
inserted
replaced
100 props.find(_._1 == name) match { |
100 props.find(_._1 == name) match { |
101 case None => None |
101 case None => None |
102 case Some((_, value)) => Value.Double.unapply(value) |
102 case Some((_, value)) => Value.Double.unapply(value) |
103 } |
103 } |
104 } |
104 } |
105 |
|
106 |
|
107 /* concrete syntax -- similar to ML */ |
|
108 |
|
109 private val syntax = Outer_Syntax.empty + "," + "(" + ")" + "[" + "]" |
|
110 |
|
111 private object Parser extends Parse.Parser |
|
112 { |
|
113 def prop: Parser[Entry] = |
|
114 keyword("(") ~ string ~ keyword(",") ~ string ~ keyword(")") ^^ |
|
115 { case _ ~ x ~ _ ~ y ~ _ => (x, y) } |
|
116 def props: Parser[T] = |
|
117 keyword("[") ~> repsep(prop, keyword(",")) <~ keyword("]") |
|
118 } |
|
119 |
|
120 def parse(text: java.lang.String): Properties.T = |
|
121 { |
|
122 Parser.parse_all(Parser.props, Token.reader(syntax.scan(text))) match { |
|
123 case Parser.Success(result, _) => result |
|
124 case bad => error(bad.toString) |
|
125 } |
|
126 } |
|
127 |
|
128 def parse_lines(prefix: java.lang.String, lines: List[java.lang.String]): List[T] = |
|
129 for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse(s) |
|
130 |
|
131 def find_parse_line(prefix: java.lang.String, lines: List[java.lang.String]): Option[T] = |
|
132 lines.find(_.startsWith(prefix)).map(line => parse(line.substring(prefix.length))) |
|
133 } |
105 } |
134 |
106 |