equal
deleted
inserted
replaced
32 message match { |
32 message match { |
33 case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) => |
33 case XML.Elem(Markup(Isabelle_Markup.STATUS, _), msgs) => |
34 (this /: msgs)((state, msg) => |
34 (this /: msgs)((state, msg) => |
35 msg match { |
35 msg match { |
36 case elem @ XML.Elem(markup, Nil) => |
36 case elem @ XML.Elem(markup, Nil) => |
37 state.add_status(markup).add_markup(Text.Info(command.range, elem)) |
37 state.add_status(markup).add_markup(Text.Info(command.range, elem)) // FIXME proper_range?? |
38 |
38 |
39 case _ => System.err.println("Ignored status message: " + msg); state |
39 case _ => System.err.println("Ignored status message: " + msg); state |
40 }) |
40 }) |
41 |
41 |
42 case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) => |
42 case XML.Elem(Markup(Isabelle_Markup.REPORT, _), msgs) => |
140 id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
140 id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") |
141 |
141 |
142 |
142 |
143 /* source text */ |
143 /* source text */ |
144 |
144 |
|
145 def length: Int = source.length |
|
146 val range: Text.Range = Text.Range(0, length) |
|
147 |
|
148 val proper_range: Text.Range = |
|
149 Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) |
|
150 |
145 def source(range: Text.Range): String = source.substring(range.start, range.stop) |
151 def source(range: Text.Range): String = source.substring(range.start, range.stop) |
146 def length: Int = source.length |
|
147 |
152 |
148 val newlines = |
153 val newlines = |
149 (0 /: Symbol.iterator(source)) { |
154 (0 /: Symbol.iterator(source)) { |
150 case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n } |
155 case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n } |
151 |
|
152 val range: Text.Range = Text.Range(0, length) |
|
153 |
156 |
154 lazy val symbol_index = new Symbol.Index(source) |
157 lazy val symbol_index = new Symbol.Index(source) |
155 def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
158 def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i) |
156 def decode(r: Text.Range): Text.Range = symbol_index.decode(r) |
159 def decode(r: Text.Range): Text.Range = symbol_index.decode(r) |
157 |
160 |