equal
deleted
inserted
replaced
3 |
3 |
4 Completion of symbols and keywords. |
4 Completion of symbols and keywords. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
|
8 |
8 |
9 |
9 import scala.collection.immutable.SortedMap |
10 import scala.collection.immutable.SortedMap |
10 import scala.util.parsing.combinator.RegexParsers |
11 import scala.util.parsing.combinator.RegexParsers |
11 import scala.math.Ordering |
12 import scala.math.Ordering |
12 |
13 |
53 val empty: History = new History() |
54 val empty: History = new History() |
54 |
55 |
55 def load(): History = |
56 def load(): History = |
56 { |
57 { |
57 def ignore_error(msg: String): Unit = |
58 def ignore_error(msg: String): Unit = |
58 java.lang.System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY + |
59 System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY + |
59 (if (msg == "") "" else "\n" + msg)) |
60 (if (msg == "") "" else "\n" + msg)) |
60 |
61 |
61 val content = |
62 val content = |
62 if (COMPLETION_HISTORY.is_file) { |
63 if (COMPLETION_HISTORY.is_file) { |
63 try { |
64 try { |