--- a/src/HOL/MicroJava/J/State.thy Fri Apr 06 19:23:51 2012 +0200
+++ b/src/HOL/MicroJava/J/State.thy Sat Apr 07 20:10:13 2012 +0200
@@ -190,9 +190,12 @@
apply simp
done
-instantiation loc' :: equal begin
+instantiation loc' :: equal
+begin
+
definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
-instance proof qed(simp add: equal_loc'_def)
+instance by default (simp add: equal_loc'_def)
+
end
end
--- a/src/HOL/MicroJava/J/Type.thy Fri Apr 06 19:23:51 2012 +0200
+++ b/src/HOL/MicroJava/J/Type.thy Sat Apr 07 20:10:13 2012 +0200
@@ -8,23 +8,40 @@
theory Type imports JBasis begin
typedecl cnam
-instantiation cnam :: equal begin
+
+instantiation cnam :: equal
+begin
+
definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'"
-instance proof qed(simp add: equal_cnam_def)
+instance by default (simp add: equal_cnam_def)
+
end
+
text {* These instantiations only ensure that the merge in theory @{text "MicroJava"} succeeds. FIXME *}
-instantiation cnam :: typerep begin
+
+instantiation cnam :: typerep
+begin
+
definition "typerep_class.typerep \<equiv> \<lambda>_ :: cnam itself. Typerep.Typerep (STR ''Type.cnam'') []"
-instance proof qed
+instance ..
+
end
-instantiation cnam :: term_of begin
+
+instantiation cnam :: term_of
+begin
+
definition "term_of_class.term_of (C :: cnam) \<equiv>
Code_Evaluation.Const (STR ''dummy_cnam'') (Typerep.Typerep (STR ''Type.cnam'') [])"
-instance proof qed
+instance ..
+
end
-instantiation cnam :: partial_term_of begin
+
+instantiation cnam :: partial_term_of
+begin
+
definition "partial_term_of_class.partial_term_of (C :: cnam itself) n = undefined"
-instance proof qed
+instance ..
+
end
-- "exceptions"
@@ -41,41 +58,73 @@
| Cname cnam
typedecl vnam -- "variable or field name"
-instantiation vnam :: equal begin
+
+instantiation vnam :: equal
+begin
+
definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'"
-instance proof qed(simp add: equal_vnam_def)
+instance by default (simp add: equal_vnam_def)
+
end
-instantiation vnam :: typerep begin
+
+instantiation vnam :: typerep
+begin
+
definition "typerep_class.typerep \<equiv> \<lambda>_ :: vnam itself. Typerep.Typerep (STR ''Type.vnam'') []"
-instance proof qed
+instance ..
+
end
-instantiation vnam :: term_of begin
+
+instantiation vnam :: term_of
+begin
+
definition "term_of_class.term_of (V :: vnam) \<equiv>
Code_Evaluation.Const (STR ''dummy_vnam'') (Typerep.Typerep (STR ''Type.vnam'') [])"
-instance proof qed
+instance ..
+
end
-instantiation vnam :: partial_term_of begin
+
+instantiation vnam :: partial_term_of
+begin
+
definition "partial_term_of_class.partial_term_of (V :: vnam itself) n = undefined"
-instance proof qed
+instance ..
+
end
typedecl mname -- "method name"
-instantiation mname :: equal begin
+
+instantiation mname :: equal
+begin
+
definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'"
-instance proof qed(simp add: equal_mname_def)
+instance by default (simp add: equal_mname_def)
+
end
-instantiation mname :: typerep begin
+
+instantiation mname :: typerep
+begin
+
definition "typerep_class.typerep \<equiv> \<lambda>_ :: mname itself. Typerep.Typerep (STR ''Type.mname'') []"
-instance proof qed
+instance ..
+
end
-instantiation mname :: term_of begin
+
+instantiation mname :: term_of
+begin
+
definition "term_of_class.term_of (M :: mname) \<equiv>
Code_Evaluation.Const (STR ''dummy_mname'') (Typerep.Typerep (STR ''Type.mname'') [])"
-instance proof qed
+instance ..
+
end
-instantiation mname :: partial_term_of begin
+
+instantiation mname :: partial_term_of
+begin
+
definition "partial_term_of_class.partial_term_of (M :: mname itself) n = undefined"
-instance proof qed
+instance ..
+
end
-- "names for @{text This} pointer and local/field variables"
--- a/src/Pure/PIDE/command.ML Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/command.ML Sat Apr 07 20:10:13 2012 +0200
@@ -6,30 +6,17 @@
signature COMMAND =
sig
- val parse_command: string -> string -> Token.T list
type 'a memo
val memo: (unit -> 'a) -> 'a memo
val memo_value: 'a -> 'a memo
val memo_eval: 'a memo -> 'a
val memo_result: 'a memo -> 'a
- val memo_stable: 'a memo -> bool
val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy
end;
structure Command: COMMAND =
struct
-(* parse command *)
-
-fun parse_command id text =
- Position.setmp_thread_data (Position.id_only id)
- (fn () =>
- let
- val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
- val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
- in toks end) ();
-
-
(* memo results *)
datatype 'a expr =
@@ -58,11 +45,6 @@
Result res => Exn.release res
| _ => raise Fail "Unfinished memo result");
-fun memo_stable (Memo v) =
- (case Synchronized.value v of
- Result (Exn.Exn exn) => not (Exn.is_interrupt exn)
- | _ => true);
-
end;
--- a/src/Pure/PIDE/document.ML Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/document.ML Sat Apr 07 20:10:13 2012 +0200
@@ -29,7 +29,7 @@
val cancel_execution: state -> Future.task list
val execute: version_id -> state -> state
val update: version_id -> version_id -> edit list -> state ->
- ((command_id * exec_id option) list * (string * command_id option) list) * state
+ (command_id * exec_id option) list * state
val remove_versions: version_id list -> state -> state
val state: unit -> state
val change_state: (state -> state) -> unit
@@ -70,17 +70,16 @@
header: node_header,
perspective: perspective,
entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*)
- last_exec: command_id option, (*last command with exec state assignment*)
result: exec}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (touched, header, perspective, entries, last_exec, result) =
+fun make_node (touched, header, perspective, entries, result) =
Node {touched = touched, header = header, perspective = perspective,
- entries = entries, last_exec = last_exec, result = result};
+ entries = entries, result = result};
-fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
- make_node (f (touched, header, perspective, entries, last_exec, result));
+fun map_node f (Node {touched, header, perspective, entries, result}) =
+ make_node (f (touched, header, perspective, entries, result));
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
@@ -88,35 +87,35 @@
val no_header = Exn.Exn (ERROR "Bad theory header");
val no_perspective = make_perspective [];
-val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_exec);
-val clear_node = map_node (fn (_, header, _, _, _, _) =>
- (false, header, no_perspective, Entries.empty, NONE, no_exec));
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, no_exec);
+val clear_node = map_node (fn (_, header, _, _, _) =>
+ (false, header, no_perspective, Entries.empty, no_exec));
(* basic components *)
fun is_touched (Node {touched, ...}) = touched;
fun set_touched touched =
- map_node (fn (_, header, perspective, entries, last_exec, result) =>
- (touched, header, perspective, entries, last_exec, result));
+ map_node (fn (_, header, perspective, entries, result) =>
+ (touched, header, perspective, entries, result));
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (touched, _, perspective, entries, last_exec, result) =>
- (touched, header, perspective, entries, last_exec, result));
+ map_node (fn (touched, _, perspective, entries, result) =>
+ (touched, header, perspective, entries, result));
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
- map_node (fn (touched, header, _, entries, last_exec, result) =>
- (touched, header, make_perspective ids, entries, last_exec, result));
+ map_node (fn (touched, header, _, entries, result) =>
+ (touched, header, make_perspective ids, entries, result));
val visible_command = #1 o get_perspective;
val visible_last = #2 o get_perspective;
val visible_node = is_some o visible_last
fun map_entries f =
- map_node (fn (touched, header, perspective, entries, last_exec, result) =>
- (touched, header, perspective, f entries, last_exec, result));
+ map_node (fn (touched, header, perspective, entries, result) =>
+ (touched, header, perspective, f entries, result));
fun get_entries (Node {entries, ...}) = entries;
fun iterate_entries f = Entries.iterate NONE f o get_entries;
@@ -125,15 +124,10 @@
NONE => I
| SOME id => Entries.iterate (SOME id) f entries);
-fun get_last_exec (Node {last_exec, ...}) = last_exec;
-fun set_last_exec last_exec =
- map_node (fn (touched, header, perspective, entries, _, result) =>
- (touched, header, perspective, entries, last_exec, result));
-
fun get_result (Node {result, ...}) = result;
fun set_result result =
- map_node (fn (touched, header, perspective, entries, last_exec, _) =>
- (touched, header, perspective, entries, last_exec, result));
+ map_node (fn (touched, header, perspective, entries, _) =>
+ (touched, header, perspective, entries, result));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -241,7 +235,7 @@
-(** document state -- content structure and execution process **)
+(** main state -- document structure and execution process **)
abstype state = State of
{versions: version Inttab.table, (*version_id -> document content*)
@@ -282,7 +276,15 @@
fun define_command (id: command_id) name text =
map_state (fn (versions, commands, execution) =>
let
- val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text);
+ val id_string = print_id id;
+ val span = Lazy.lazy (fn () =>
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () =>
+ Thy_Syntax.parse_tokens
+ (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+ val _ =
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) ();
val commands' =
Inttab.update_new (id, (name, span)) commands
handle Inttab.DUP dup => err_dup "command" dup;
@@ -304,13 +306,19 @@
-(** execute **)
+(** edit operations **)
+
+(* execute *)
+
+local
fun finished_theory node =
(case Exn.capture Command.memo_result (get_result node) of
Exn.Res (st, _) => can (Toplevel.end_theory Position.none) st
| _ => false);
+in
+
fun execute version_id state =
state |> map_state (fn (versions, commands, _) =>
let
@@ -345,15 +353,27 @@
in (versions, commands, (version_id, group, running)) end);
-
+end;
-(** edits **)
-
(* update *)
local
+fun stable_finished_theory node =
+ is_some (Exn.get_res (Exn.capture (fn () =>
+ fst (Command.memo_result (get_result node))
+ |> Toplevel.end_theory Position.none
+ |> Global_Theory.join_proofs) ()));
+
+fun stable_command exec =
+ (case Exn.capture Command.memo_result exec of
+ Exn.Exn exn => not (Exn.is_interrupt exn)
+ | Exn.Res (st, _) =>
+ (case try Toplevel.theory_of st of
+ NONE => true
+ | SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy))));
+
fun make_required nodes =
let
val all_visible =
@@ -406,7 +426,7 @@
(case opt_exec of
NONE => true
| SOME (exec_id, exec) =>
- not (Command.memo_stable exec) orelse
+ not (stable_command exec) orelse
(case lookup_entry node0 id of
NONE => true
| SOME (exec_id0, _) => exec_id <> exec_id0));
@@ -459,7 +479,7 @@
val updated =
nodes |> Graph.schedule
(fn deps => fn (name, node) =>
- if is_touched node orelse is_required name andalso not (finished_theory node) then
+ if is_touched node orelse is_required name andalso not (stable_finished_theory node) then
let
val node0 = node_of old_version name;
fun init () = init_theory deps node;
@@ -499,7 +519,6 @@
val node' = node
|> fold reset_entry no_execs
|> fold (fn (id, exec) => update_entry id (SOME exec)) execs
- |> set_last_exec last_exec
|> set_result result
|> set_touched false;
in ((no_execs, execs, [(name, node')]), node') end)
@@ -511,11 +530,10 @@
map (rpair NONE) (maps #1 updated) @
map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
val updated_nodes = maps #3 updated;
- val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
val state' = state
|> define_version new_id (fold put_node updated_nodes new_version);
- in ((command_execs, last_execs), state') end;
+ in (command_execs, state') end;
end;
--- a/src/Pure/PIDE/document.scala Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/document.scala Sat Apr 07 20:10:13 2012 +0200
@@ -296,9 +296,7 @@
result: PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
- type Assign =
- (List[(Document.Command_ID, Option[Document.Exec_ID])], // exec state assignment
- List[(String, Option[Document.Command_ID])]) // last exec
+ type Assign = List[(Document.Command_ID, Option[Document.Exec_ID])] // exec state assignment
object State
{
@@ -311,14 +309,12 @@
final class Assignment private(
val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
- val last_execs: Map[String, Option[Command_ID]] = Map.empty,
val is_finished: Boolean = false)
{
def check_finished: Assignment = { require(is_finished); this }
- def unfinished: Assignment = new Assignment(command_execs, last_execs, false)
+ def unfinished: Assignment = new Assignment(command_execs, false)
- def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
- add_last_execs: List[(String, Option[Command_ID])]): Assignment =
+ def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])]): Assignment =
{
require(!is_finished)
val command_execs1 =
@@ -326,7 +322,7 @@
case (res, (command_id, None)) => res - command_id
case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
}
- new Assignment(command_execs1, last_execs ++ add_last_execs, true)
+ new Assignment(command_execs1, true)
}
}
@@ -368,7 +364,7 @@
}
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
- def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename
+ def the_command_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
@@ -387,15 +383,14 @@
}
}
- def assign(id: Version_ID, arg: Assign = (Nil, Nil)): (List[Command], State) =
+ def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
{
val version = the_version(id)
- val (command_execs, last_execs) = arg
val (changed_commands, new_execs) =
((Nil: List[Command], execs) /: command_execs) {
case ((commands1, execs1), (cmd_id, exec)) =>
- val st = the_command(cmd_id)
+ val st = the_command_state(cmd_id)
val commands2 = st.command :: commands1
val execs2 =
exec match {
@@ -404,7 +399,7 @@
}
(commands2, execs2)
}
- val new_assignment = the_assignment(version).assign(command_execs, last_execs)
+ val new_assignment = the_assignment(version).assign(command_execs)
val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
(changed_commands, new_state)
@@ -424,21 +419,6 @@
def tip_stable: Boolean = is_stable(history.tip)
def tip_version: Version = history.tip.version.get_finished
- def last_exec_offset(name: Node.Name): Text.Offset =
- {
- val version = tip_version
- the_assignment(version).last_execs.get(name.node) match {
- case Some(Some(id)) =>
- val node = version.nodes(name)
- val cmd = the_command(id).command
- node.command_start(cmd) match {
- case None => 0
- case Some(start) => start + cmd.length
- }
- case _ => 0
- }
- }
-
def continue_history(
previous: Future[Version],
edits: List[Edit_Text],
@@ -490,7 +470,11 @@
the_exec(the_assignment(version).check_finished.command_execs
.getOrElse(command.id, fail))
}
- catch { case _: State.Fail => command.empty_state }
+ catch {
+ case _: State.Fail =>
+ try { the_command_state(command.id) }
+ catch { case _: State.Fail => command.empty_state }
+ }
}
--- a/src/Pure/PIDE/isabelle_markup.ML Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Sat Apr 07 20:10:13 2012 +0200
@@ -90,7 +90,7 @@
val sendbackN: string val sendback: Markup.T
val hiliteN: string val hilite: Markup.T
val taskN: string
- val parsedN: string val parsed: Markup.T
+ val acceptedN: string val accepted: Markup.T
val forkedN: string val forked: Markup.T
val joinedN: string val joined: Markup.T
val failedN: string val failed: Markup.T
@@ -283,7 +283,7 @@
val taskN = "task";
-val (parsedN, parsed) = markup_elem "parsed";
+val (acceptedN, accepted) = markup_elem "accepted";
val (forkedN, forked) = markup_elem "forked";
val (joinedN, joined) = markup_elem "joined";
--- a/src/Pure/PIDE/isabelle_markup.scala Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Sat Apr 07 20:10:13 2012 +0200
@@ -198,7 +198,7 @@
val TASK = "task"
- val PARSED = "parsed"
+ val ACCEPTED = "accepted"
val FORKED = "forked"
val JOINED = "joined"
val FAILED = "failed"
--- a/src/Pure/PIDE/protocol.ML Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Sat Apr 07 20:10:13 2012 +0200
@@ -55,7 +55,7 @@
Output.protocol_message Isabelle_Markup.assign_execs
((new_id, assignment) |>
let open XML.Encode
- in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
+ in pair int (list (pair int (option int))) end
|> YXML.string_of_body);
val state2 = Document.execute new_id state1;
in state2 end));
--- a/src/Pure/PIDE/protocol.scala Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Sat Apr 07 20:10:13 2012 +0200
@@ -17,7 +17,7 @@
try {
import XML.Decode._
val body = YXML.parse_body(text)
- Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
+ Some(pair(long, list(pair(long, option(long))))(body))
}
catch {
case ERROR(_) => None
@@ -49,27 +49,27 @@
}
sealed case class Status(
- private val parsed: Boolean = false,
+ private val accepted: Boolean = false,
private val finished: Boolean = false,
private val failed: Boolean = false,
forks: Int = 0)
{
- def is_unprocessed: Boolean = parsed && !finished && !failed && forks == 0
+ def is_unprocessed: Boolean = accepted && !finished && !failed && forks == 0
def is_running: Boolean = forks != 0
def is_finished: Boolean = finished && forks == 0
def is_failed: Boolean = failed && forks == 0
def + (that: Status): Status =
- Status(parsed || that.parsed, finished || that.finished,
+ Status(accepted || that.accepted, finished || that.finished,
failed || that.failed, forks + that.forks)
}
val command_status_markup: Set[String] =
- Set(Isabelle_Markup.PARSED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
+ Set(Isabelle_Markup.ACCEPTED, Isabelle_Markup.FINISHED, Isabelle_Markup.FAILED,
Isabelle_Markup.FORKED, Isabelle_Markup.JOINED)
def command_status(status: Status, markup: Markup): Status =
markup match {
- case Markup(Isabelle_Markup.PARSED, _) => status.copy(parsed = true)
+ case Markup(Isabelle_Markup.ACCEPTED, _) => status.copy(accepted = true)
case Markup(Isabelle_Markup.FINISHED, _) => status.copy(finished = true)
case Markup(Isabelle_Markup.FAILED, _) => status.copy(failed = true)
case Markup(Isabelle_Markup.FORKED, _) => status.copy(forks = status.forks + 1)
--- a/src/Pure/System/isabelle_process.ML Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML Sat Apr 07 20:10:13 2012 +0200
@@ -167,8 +167,8 @@
val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
val _ = Output.physical_stderr Symbol.STX;
- val _ = quick_and_dirty := true;
- val _ = Goal.parallel_proofs := 0;
+ val _ = quick_and_dirty := false;
+ val _ = Goal.parallel_proofs := 1;
val _ =
if Multithreading.max_threads_value () < 2
then Multithreading.max_threads := 2 else ();
--- a/src/Pure/System/session.scala Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Pure/System/session.scala Sat Apr 07 20:10:13 2012 +0200
@@ -399,7 +399,7 @@
case _ =>
if (output.is_exit && phase == Session.Startup) phase = Session.Failed
else if (output.is_exit) phase = Session.Inactive
- else if (output.is_stdout) { }
+ else if (output.is_init || output.is_stdout) { }
else bad_output(output)
}
}
--- a/src/Tools/jEdit/src/document_model.scala Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Sat Apr 07 20:10:13 2012 +0200
@@ -95,7 +95,6 @@
private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
- private var pending_perspective = false
private var last_perspective: Text.Perspective = Text.Perspective.empty
def snapshot(): List[Text.Edit] = pending.toList
@@ -104,16 +103,12 @@
{
Swing_Thread.require()
- val new_perspective =
- if (pending_perspective) { pending_perspective = false; perspective() }
- else last_perspective
-
- snapshot() match {
- case Nil if last_perspective == new_perspective =>
- case edits =>
- pending.clear
- last_perspective = new_perspective
- session.edit_node(name, node_header(), new_perspective, edits)
+ val edits = snapshot()
+ val new_perspective = perspective()
+ if (!edits.isEmpty || last_perspective != new_perspective) {
+ pending.clear
+ last_perspective = new_perspective
+ session.edit_node(name, node_header(), new_perspective, edits)
}
}
@@ -129,7 +124,6 @@
def update_perspective()
{
- pending_perspective = true
delay_flush(true)
}
--- a/src/Tools/jEdit/src/document_view.scala Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Sat Apr 07 20:10:13 2012 +0200
@@ -27,8 +27,7 @@
import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
- ScrollListener}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.{SyntaxStyle}
--- a/src/Tools/jEdit/src/modes/isabelle.xml Fri Apr 06 19:23:51 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle.xml Sat Apr 07 20:10:13 2012 +0200
@@ -33,6 +33,7 @@
<KEYWORD2>header</KEYWORD2>
<KEYWORD1>theory</KEYWORD1>
<KEYWORD2>imports</KEYWORD2>
+ <KEYWORD2>keywords</KEYWORD2>
<KEYWORD2>uses</KEYWORD2>
<KEYWORD2>begin</KEYWORD2>
<KEYWORD2>end</KEYWORD2>