# HG changeset patch # User wenzelm # Date 1333823701 -7200 # Node ID 84d8952b5bd97f916c89d3511ca49f0184225e39 # Parent b7625245a846d3299169faf7f996b7d298ea6258# Parent 8a5a1d26337fbca0a21ae78d1fc030c89d1fb580 merged diff -r b7625245a846 -r 84d8952b5bd9 src/HOL/MicroJava/J/State.thy --- a/src/HOL/MicroJava/J/State.thy Sat Apr 07 20:24:39 2012 +0200 +++ b/src/HOL/MicroJava/J/State.thy Sat Apr 07 20:35:01 2012 +0200 @@ -190,9 +190,12 @@ apply simp done -instantiation loc' :: equal begin +instantiation loc' :: equal +begin + definition "HOL.equal (l :: loc') l' \ l = l'" -instance proof qed(simp add: equal_loc'_def) +instance by default (simp add: equal_loc'_def) + end end diff -r b7625245a846 -r 84d8952b5bd9 src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Sat Apr 07 20:24:39 2012 +0200 +++ b/src/HOL/MicroJava/J/Type.thy Sat Apr 07 20:35:01 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' \ 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 \ \_ :: 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) \ 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' \ 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 \ \_ :: 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) \ 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' \ 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 \ \_ :: 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) \ 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" diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/command.ML Sat Apr 07 20:35:01 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; diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/document.ML Sat Apr 07 20:35:01 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; diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/document.scala Sat Apr 07 20:35:01 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 } + } } diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/isabelle_markup.ML --- a/src/Pure/PIDE/isabelle_markup.ML Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.ML Sat Apr 07 20:35:01 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"; diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/isabelle_markup.scala --- a/src/Pure/PIDE/isabelle_markup.scala Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/isabelle_markup.scala Sat Apr 07 20:35:01 2012 +0200 @@ -198,7 +198,7 @@ val TASK = "task" - val PARSED = "parsed" + val ACCEPTED = "accepted" val FORKED = "forked" val JOINED = "joined" val FAILED = "failed" diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/protocol.ML Sat Apr 07 20:35:01 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)); diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/PIDE/protocol.scala Sat Apr 07 20:35:01 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) diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/System/isabelle_process.ML Sat Apr 07 20:35:01 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 (); diff -r b7625245a846 -r 84d8952b5bd9 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Pure/System/session.scala Sat Apr 07 20:35:01 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) } } diff -r b7625245a846 -r 84d8952b5bd9 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Apr 07 20:35:01 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) } diff -r b7625245a846 -r 84d8952b5bd9 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Sat Apr 07 20:35:01 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} diff -r b7625245a846 -r 84d8952b5bd9 src/Tools/jEdit/src/modes/isabelle.xml --- a/src/Tools/jEdit/src/modes/isabelle.xml Sat Apr 07 20:24:39 2012 +0200 +++ b/src/Tools/jEdit/src/modes/isabelle.xml Sat Apr 07 20:35:01 2012 +0200 @@ -33,6 +33,7 @@ header theory imports + keywords uses begin end