--- a/src/Pure/General/markup.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/markup.ML Wed Sep 01 13:45:58 2010 +0200
@@ -14,8 +14,8 @@
val properties: Properties.T -> T -> T
val nameN: string
val name: string -> T -> T
+ val kindN: string
val bindingN: string val binding: string -> T
- val kindN: string
val entityN: string val entity: string -> T
val defN: string
val refN: string
@@ -115,8 +115,10 @@
val assignN: string val assign: int -> T
val editN: string val edit: int -> int -> T
val pidN: string
+ val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
+ val reportN: string val report: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -163,13 +165,12 @@
val nameN = "name";
fun name a = properties [(nameN, a)];
-val (bindingN, binding) = markup_string "binding" nameN;
-
val kindN = "kind";
(* formal entities *)
+val (bindingN, binding) = markup_string "binding" nameN;
val (entityN, entity) = markup_string "entity" nameN;
val defN = "def";
@@ -337,10 +338,13 @@
(* messages *)
val pidN = "pid";
+val serialN = "serial";
val (promptN, prompt) = markup_elem "prompt";
val (readyN, ready) = markup_elem "ready";
+val (reportN, report) = markup_elem "report";
+
(** print mode operations **)
--- a/src/Pure/General/markup.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/markup.scala Wed Sep 01 13:45:58 2010 +0200
@@ -69,6 +69,7 @@
/* formal entities */
+ val BINDING = "binding"
val ENTITY = "entity"
val DEF = "def"
val REF = "ref"
@@ -226,6 +227,7 @@
/* messages */
val PID = "pid"
+ val Serial = new Long_Property("serial")
val MESSAGE = "message"
val CLASS = "class"
--- a/src/Pure/General/position.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/position.ML Wed Sep 01 13:45:58 2010 +0200
@@ -27,6 +27,7 @@
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
val default_properties: T -> Properties.T -> Properties.T
+ val report_markup: T -> Markup.T
val report_text: Markup.T -> T -> string -> unit
val report: Markup.T -> T -> unit
val str_of: T -> string
@@ -125,6 +126,8 @@
if exists (member (op =) Markup.position_properties o #1) props then props
else properties_of default @ props;
+fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+
fun report_text markup (pos as Pos (count, _)) txt =
if invalid_count count then ()
else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
--- a/src/Pure/General/position.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/position.scala Wed Sep 01 13:45:58 2010 +0200
@@ -28,4 +28,15 @@
case _ => None
}
}
+
+ object Id_Range
+ {
+ def unapply(pos: T): Option[(Long, Text.Range)] =
+ (pos, pos) match {
+ case (Id(id), Range(range)) => Some((id, range))
+ case _ => None
+ }
+ }
+
+ def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
}
--- a/src/Pure/General/scan.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/scan.ML Wed Sep 01 13:45:58 2010 +0200
@@ -105,7 +105,7 @@
fun catch scan xs = scan xs
handle ABORT msg => raise Fail msg
- | FAIL msg => raise Fail (the_default "Syntax error." msg);
+ | FAIL msg => raise Fail (the_default "Syntax error" msg);
(* scanner combinators *)
--- a/src/Pure/General/symbol.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/symbol.scala Wed Sep 01 13:45:58 2010 +0200
@@ -53,6 +53,9 @@
def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || '\ud800' <= c && c <= '\udfff')
+ def is_physical_newline(s: CharSequence): Boolean =
+ "\n".contentEquals(s) || "\r".contentEquals(s) || "\r\n".contentEquals(s)
+
def is_wellformed(s: CharSequence): Boolean =
s.length == 1 && is_plain(s.charAt(0)) || !bad_symbol.pattern.matcher(s).matches
--- a/src/Pure/General/xml.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/General/xml.scala Wed Sep 01 13:45:58 2010 +0200
@@ -102,17 +102,19 @@
x
}
+ def trim_bytes(s: String): String = new String(s.toCharArray)
+
def cache_string(x: String): String =
lookup(x) match {
case Some(y) => y
- case None => store(new String(x.toCharArray)) // trim string value
+ case None => store(trim_bytes(x))
}
def cache_props(x: List[(String, String)]): List[(String, String)] =
if (x.isEmpty) x
else
lookup(x) match {
case Some(y) => y
- case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2))))
+ case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2))))
}
def cache_markup(x: Markup): Markup =
lookup(x) match {
--- a/src/Pure/Isar/class_declaration.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Isar/class_declaration.ML Wed Sep 01 13:45:58 2010 +0200
@@ -126,8 +126,8 @@
else error ("Type inference imposes additional sort constraint "
^ Syntax.string_of_sort_global thy inferred_sort
^ " of type parameter " ^ Name.aT ^ " of sort "
- ^ Syntax.string_of_sort_global thy a_sort ^ ".")
- | _ => error "Multiple type variables in class specification.";
+ ^ Syntax.string_of_sort_global thy a_sort)
+ | _ => error "Multiple type variables in class specification";
in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
val after_infer_fixate = (map o map_atyps)
(fn T as TFree _ => T | T as TVar (vi, sort) =>
--- a/src/Pure/Isar/isar_cmd.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Sep 01 13:45:58 2010 +0200
@@ -44,7 +44,6 @@
val pwd: Toplevel.transition -> Toplevel.transition
val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
- val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
val print_context: Toplevel.transition -> Toplevel.transition
val print_theory: bool -> Toplevel.transition -> Toplevel.transition
val print_syntax: Toplevel.transition -> Toplevel.transition
@@ -321,11 +320,6 @@
in File.isabelle_tool "print" ("-c " ^ outfile); () end);
-(* pretty_setmargin *)
-
-fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.margin_default := n);
-
-
(* print parts of theory and proof context *)
val print_context = Toplevel.keep Toplevel.print_state_context;
--- a/src/Pure/Isar/isar_syn.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Sep 01 13:45:58 2010 +0200
@@ -786,7 +786,8 @@
val _ =
Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
- Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
+ Keyword.diag (Parse.nat >>
+ (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
val _ =
Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
@@ -991,7 +992,7 @@
(Scan.succeed
(Toplevel.no_timing o Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
- raise Toplevel.TERMINATE))));
+ raise Runtime.TERMINATE))));
end;
--- a/src/Pure/Isar/obtain.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Sep 01 13:45:58 2010 +0200
@@ -181,7 +181,7 @@
if Thm.concl_of th aconv thesis andalso
Logic.strip_assums_concl prem aconv thesis then th
else error ("Guessed a different clause:\n" ^ Display.string_of_thm ctxt th)
- | [] => error "Goal solved -- nothing guessed."
+ | [] => error "Goal solved -- nothing guessed"
| _ => error ("Guess split into several cases:\n" ^ Display.string_of_thm ctxt th));
fun result tac facts ctxt =
--- a/src/Pure/Isar/runtime.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Wed Sep 01 13:45:58 2010 +0200
@@ -11,6 +11,7 @@
exception EXCURSION_FAIL of exn * string
exception TOPLEVEL_ERROR
val exn_context: Proof.context option -> exn -> exn
+ val exn_messages: (exn -> Position.T) -> exn -> string list
val exn_message: (exn -> Position.T) -> exn -> string
val debugging: ('a -> 'b) -> 'a -> 'b
val controlled_execution: ('a -> 'b) -> 'a -> 'b
@@ -41,7 +42,7 @@
fun if_context NONE _ _ = []
| if_context (SOME ctxt) f xs = map (f ctxt) xs;
-fun exn_message exn_position e =
+fun exn_messages exn_position e =
let
fun raised exn name msgs =
let val pos = Position.str_of (exn_position exn) in
@@ -53,32 +54,36 @@
val detailed = ! Output.debugging;
- fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn
- | exn_msg _ (Exn.EXCEPTIONS []) = "Exception."
- | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns)
- | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) =
- exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc)
- | exn_msg _ TERMINATE = "Exit."
- | exn_msg _ Exn.Interrupt = "Interrupt."
- | exn_msg _ TimeLimit.TimeOut = "Timeout."
- | exn_msg _ TOPLEVEL_ERROR = "Error."
- | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
- | exn_msg _ (ERROR msg) = msg
- | exn_msg _ (exn as Fail msg) = raised exn "Fail" [msg]
- | exn_msg _ (exn as THEORY (msg, thys)) =
- raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))
- | exn_msg _ (exn as Syntax.AST (msg, asts)) = raised exn "AST" (msg ::
- (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))
- | exn_msg ctxt (exn as TYPE (msg, Ts, ts)) = raised exn "TYPE" (msg ::
+ fun exn_msgs _ (CONTEXT (ctxt, exn)) = exn_msgs (SOME ctxt) exn
+ | exn_msgs ctxt (Exn.EXCEPTIONS exns) = maps (exn_msgs ctxt) exns
+ | exn_msgs ctxt (EXCURSION_FAIL (exn, loc)) =
+ map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs ctxt exn)
+ | exn_msgs _ TERMINATE = ["Exit"]
+ | exn_msgs _ Exn.Interrupt = []
+ | exn_msgs _ TimeLimit.TimeOut = ["Timeout"]
+ | exn_msgs _ TOPLEVEL_ERROR = ["Error"]
+ | exn_msgs _ (SYS_ERROR msg) = ["## SYSTEM ERROR ##\n" ^ msg]
+ | exn_msgs _ (ERROR msg) = [msg]
+ | exn_msgs _ (exn as Fail msg) = [raised exn "Fail" [msg]]
+ | exn_msgs _ (exn as THEORY (msg, thys)) =
+ [raised exn "THEORY" (msg :: (if detailed then map Context.str_of_thy thys else []))]
+ | exn_msgs _ (exn as Syntax.AST (msg, asts)) = [raised exn "AST" (msg ::
+ (if detailed then map (Pretty.string_of o Syntax.pretty_ast) asts else []))]
+ | exn_msgs ctxt (exn as TYPE (msg, Ts, ts)) = [raised exn "TYPE" (msg ::
(if detailed then
if_context ctxt Syntax.string_of_typ Ts @ if_context ctxt Syntax.string_of_term ts
- else []))
- | exn_msg ctxt (exn as TERM (msg, ts)) = raised exn "TERM" (msg ::
- (if detailed then if_context ctxt Syntax.string_of_term ts else []))
- | exn_msg ctxt (exn as THM (msg, i, thms)) = raised exn ("THM " ^ string_of_int i) (msg ::
- (if detailed then if_context ctxt Display.string_of_thm thms else []))
- | exn_msg _ exn = raised exn (General.exnMessage exn) [];
- in exn_msg NONE e end;
+ else []))]
+ | exn_msgs ctxt (exn as TERM (msg, ts)) = [raised exn "TERM" (msg ::
+ (if detailed then if_context ctxt Syntax.string_of_term ts else []))]
+ | exn_msgs ctxt (exn as THM (msg, i, thms)) = [raised exn ("THM " ^ string_of_int i) (msg ::
+ (if detailed then if_context ctxt Display.string_of_thm thms else []))]
+ | exn_msgs _ exn = [raised exn (General.exnMessage exn) []];
+ in exn_msgs NONE e end;
+
+fun exn_message exn_position exn =
+ (case exn_messages exn_position exn of
+ [] => "Interrupt"
+ | msgs => cat_lines msgs);
--- a/src/Pure/Isar/toplevel.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Sep 01 13:45:58 2010 +0200
@@ -30,19 +30,20 @@
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
val skip_proofs: bool Unsynchronized.ref
- exception TERMINATE
exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
val thread: bool -> (unit -> unit) -> Thread.thread
type transition
val empty: transition
val init_of: transition -> string option
+ val print_of: transition -> bool
val name_of: transition -> string
val pos_of: transition -> Position.T
val str_of: transition -> string
val name: string -> transition -> transition
val position: Position.T -> transition -> transition
val interactive: bool -> transition -> transition
+ val set_print: bool -> transition -> transition
val print: transition -> transition
val no_timing: transition -> transition
val init_theory: string -> (unit -> theory) -> transition -> transition
@@ -84,10 +85,9 @@
val unknown_context: transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val status: transition -> Markup.T -> unit
- val error_msg: transition -> exn * string -> unit
+ val error_msg: transition -> string -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
- val run_command: string -> transition -> state -> state option
val command: transition -> state -> state
val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
end;
@@ -222,8 +222,6 @@
val profiling = Unsynchronized.ref 0;
val skip_proofs = Unsynchronized.ref false;
-exception TERMINATE = Runtime.TERMINATE;
-exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
fun program body =
@@ -351,12 +349,13 @@
fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
| init_of _ = NONE;
+fun print_of (Transition {print, ...}) = print;
fun name_of (Transition {name, ...}) = name;
fun pos_of (Transition {pos, ...}) = pos;
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
fun command_msg msg tr = msg ^ "command " ^ str_of tr;
-fun at_command tr = command_msg "At " tr ^ ".";
+fun at_command tr = command_msg "At " tr;
fun type_error tr state =
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
@@ -563,9 +562,8 @@
fun status tr m =
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) ();
-fun error_msg tr exn_info =
- setmp_thread_position tr (fn () =>
- Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) ();
+fun error_msg tr msg =
+ setmp_thread_position tr (fn () => Output.error_msg msg) ();
(* post-transition hooks *)
@@ -609,8 +607,8 @@
val ctxt = try context_of st;
val res =
(case app int tr st of
- (_, SOME TERMINATE) => NONE
- | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
+ (_, SOME Runtime.TERMINATE) => NONE
+ | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
| (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
| (st', NONE) => SOME (st', NONE));
val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
@@ -619,53 +617,13 @@
end;
-(* managed execution *)
-
-local
-
-fun async_state (tr as Transition {print, ...}) st =
- if print then
- ignore
- (Future.fork (fn () =>
- setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
- else ();
-
-fun proof_status tr st =
- (case try proof_of st of
- SOME prf => status tr (Proof.status_markup prf)
- | NONE => ());
-
-in
-
-fun run_command thy_name tr st =
- (case
- (case init_of tr of
- SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
- | NONE => Exn.Result ()) of
- Exn.Result () =>
- let val int = is_some (init_of tr) in
- (case transition int tr st of
- SOME (st', NONE) =>
- (status tr Markup.finished;
- proof_status tr st';
- if int then () else async_state tr st';
- SOME st')
- | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
- | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
- | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
- end
- | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
-
-end;
-
-
(* nested commands *)
fun command tr st =
(case transition (! interact) tr st of
SOME (st', NONE) => st'
- | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info
- | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
+ | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
+ | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
fun command_result tr st =
let val st' = command tr st
--- a/src/Pure/ML/ml_compiler.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/ML/ml_compiler.ML Wed Sep 01 13:45:58 2010 +0200
@@ -7,6 +7,7 @@
signature ML_COMPILER =
sig
val exn_position: exn -> Position.T
+ val exn_messages: exn -> string list
val exn_message: exn -> string
val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
@@ -15,6 +16,7 @@
struct
fun exn_position _ = Position.none;
+val exn_messages = Runtime.exn_messages exn_position;
val exn_message = Runtime.exn_message exn_position;
fun eval verbose pos toks =
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Wed Sep 01 13:45:58 2010 +0200
@@ -4,13 +4,6 @@
Advanced runtime compilation for Poly/ML 5.3.0.
*)
-signature ML_COMPILER =
-sig
- val exn_position: exn -> Position.T
- val exn_message: exn -> string
- val eval: bool -> Position.T -> ML_Lex.token list -> unit
-end
-
structure ML_Compiler: ML_COMPILER =
struct
@@ -37,6 +30,7 @@
NONE => Position.none
| SOME loc => position_of loc);
+val exn_messages = Runtime.exn_messages exn_position;
val exn_message = Runtime.exn_message exn_position;
--- a/src/Pure/PIDE/command.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/PIDE/command.scala Wed Sep 01 13:45:58 2010 +0200
@@ -8,23 +8,25 @@
package isabelle
+import scala.collection.immutable.SortedMap
+
+
object Command
{
/** accumulated results from prover **/
case class State(
val command: Command,
- val status: List[Markup],
- val reverse_results: List[XML.Tree],
- val markup: Markup_Tree)
+ val status: List[Markup] = Nil,
+ val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
+ val markup: Markup_Tree = Markup_Tree.empty)
{
/* content */
- lazy val results = reverse_results.reverse
-
def add_status(st: Markup): State = copy(status = st :: status)
def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
- def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
+ def add_result(serial: Long, result: XML.Tree): State =
+ copy(results = results + (serial -> result))
def root_info: Text.Info[Any] =
new Text.Info(command.range,
@@ -34,7 +36,7 @@
/* message dispatch */
- def accumulate(message: XML.Tree): Command.State =
+ def accumulate(message: XML.Elem): Command.State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -46,15 +48,22 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
- if Position.Id.unapply(atts) == Some(command.id) =>
- val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+ case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
+ if id == command.id =>
+ val props = Position.purge(atts)
val info =
Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
state.add_markup(info)
case _ => System.err.println("Ignored report message: " + msg); state
})
- case _ => add_result(message)
+ case XML.Elem(Markup(name, atts), body) =>
+ atts match {
+ case Markup.Serial(i) =>
+ val result = XML.Elem(Markup(name, Position.purge(atts)), body)
+ (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
+ (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+ case _ => System.err.println("Ignored message without serial number: " + message); this
+ }
}
}
@@ -89,6 +98,10 @@
def source(range: Text.Range): String = source.substring(range.start, range.stop)
def length: Int = source.length
+ val newlines =
+ (0 /: Symbol.iterator(source)) {
+ case (n, s) => if (Symbol.is_physical_newline(s)) n + 1 else n }
+
val range: Text.Range = Text.Range(0, length)
lazy val symbol_index = new Symbol.Index(source)
@@ -98,5 +111,5 @@
/* accumulated results */
- val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
+ val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/document.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/PIDE/document.ML Wed Sep 01 13:45:58 2010 +0200
@@ -192,6 +192,59 @@
+(* toplevel transactions *)
+
+local
+
+fun proof_status tr st =
+ (case try Toplevel.proof_of st of
+ SOME prf => Toplevel.status tr (Proof.status_markup prf)
+ | NONE => ());
+
+fun async_state tr st =
+ if Toplevel.print_of tr then
+ ignore
+ (Future.fork
+ (fn () =>
+ Toplevel.setmp_thread_position tr
+ (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
+ else ();
+
+in
+
+fun run_command thy_name tr st =
+ (case
+ (case Toplevel.init_of tr of
+ SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
+ | NONE => Exn.Result ()) of
+ Exn.Result () =>
+ let
+ val int = is_some (Toplevel.init_of tr);
+ val (errs, result) =
+ (case Toplevel.transition int tr st of
+ SOME (st', NONE) => ([], SOME st')
+ | SOME (_, SOME exn_info) =>
+ (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+ [] => raise Exn.Interrupt
+ | errs => (errs, NONE))
+ | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+ val _ = List.app (Toplevel.error_msg tr) errs;
+ val _ =
+ (case result of
+ NONE => Toplevel.status tr Markup.failed
+ | SOME st' =>
+ (Toplevel.status tr Markup.finished;
+ proof_status tr st';
+ if int then () else async_state tr st'));
+ in result end
+ | Exn.Exn exn =>
+ (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+
+end;
+
+
+
+
(** editing **)
(* edit *)
@@ -214,7 +267,7 @@
NONE => NONE
| SOME st =>
let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
- in Toplevel.run_command name exec_tr st end));
+ in run_command name exec_tr st end));
val state' = define_exec exec_id' exec' state;
in (exec_id', (id, exec_id') :: updates, state') end;
@@ -263,7 +316,8 @@
| force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
val _ = List.app Future.cancel execution;
- fun await_cancellation () = uninterruptible (fn _ => Future.join_results) execution;
+ fun await_cancellation () =
+ uninterruptible (fn _ => fn () => Future.join_results execution) ();
val execution' = (* FIXME proper node deps *)
node_names_of version |> map (fn name =>
--- a/src/Pure/PIDE/document.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/PIDE/document.scala Wed Sep 01 13:45:58 2010 +0200
@@ -44,7 +44,6 @@
{
val empty: Node = new Node(Linear_Set())
- // FIXME not scalable
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
{
@@ -57,16 +56,36 @@
}
}
+ private val block_size = 1024
+
class Node(val commands: Linear_Set[Command])
{
- def command_starts: Iterator[(Command, Text.Offset)] =
- Node.command_starts(commands.iterator)
+ private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
+ {
+ val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
+ var next_block = 0
+ var last_stop = 0
+ for ((command, start) <- Node.command_starts(commands.iterator)) {
+ last_stop = start + command.length
+ while (last_stop + 1 > next_block) {
+ blocks += (command -> start)
+ next_block += block_size
+ }
+ }
+ (blocks.toArray, Text.Range(0, last_stop))
+ }
- def command_start(cmd: Command): Option[Text.Offset] =
- command_starts.find(_._1 == cmd).map(_._2)
+ def full_range: Text.Range = full_index._2
def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
- command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+ {
+ if (!commands.isEmpty && full_range.contains(i)) {
+ val (cmd0, start0) = full_index._1(i / block_size)
+ Node.command_starts(commands.iterator(cmd0), start0) dropWhile {
+ case (cmd, start) => start + cmd.length <= i }
+ }
+ else Iterator.empty
+ }
def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] =
command_range(range.start) takeWhile { case (_, start) => start < range.stop }
@@ -83,6 +102,12 @@
commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
case None => None
}
+
+ def command_start(cmd: Command): Option[Text.Offset] =
+ command_starts.find(_._1 == cmd).map(_._2)
+
+ def command_starts: Iterator[(Command, Text.Offset)] =
+ Node.command_starts(commands.iterator)
}
@@ -155,7 +180,7 @@
{
class Fail(state: State) extends Exception
- val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
+ val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
class Assignment(former_assignment: Map[Command, Exec_ID])
{
@@ -204,7 +229,7 @@
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
- def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
+ def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some((st, occs)) =>
val new_st = st.accumulate(message)
@@ -218,7 +243,7 @@
}
}
- def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
+ def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
{
val version = the_version(id)
val occs = Set(version) // FIXME unused (!?)
@@ -232,7 +257,7 @@
(st.command, exec_id)
}
the_assignment(version).assign(assigned_execs) // FIXME explicit value instead of promise (!?)
- copy(execs = new_execs)
+ (assigned_execs.map(_._1), copy(execs = new_execs))
}
def is_assigned(version: Version): Boolean =
--- a/src/Pure/PIDE/isar_document.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Wed Sep 01 13:45:58 2010 +0200
@@ -54,6 +54,22 @@
else if (markup.exists(_.name == Markup.FINISHED)) Finished
else Unprocessed
}
+
+
+ /* reported positions */
+
+ def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+ {
+ def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+ tree match {
+ case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
+ if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
+ id == command_id => body.foldLeft(set + range)(reported)
+ case XML.Elem(_, body) => body.foldLeft(set)(reported)
+ case XML.Text(_) => set
+ }
+ reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
+ }
}
--- a/src/Pure/ROOT.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Sep 01 13:45:58 2010 +0200
@@ -179,9 +179,9 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "Isar/runtime.ML";
+use "ML/ml_compiler.ML";
if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1" orelse
- String.isPrefix "smlnj" ml_system
-then use "ML/ml_compiler.ML"
+ String.isPrefix "smlnj" ml_system then ()
else use "ML/ml_compiler_polyml-5.3.ML";
use "ML/ml_context.ML";
--- a/src/Pure/Syntax/parser.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Syntax/parser.ML Wed Sep 01 13:45:58 2010 +0200
@@ -773,7 +773,7 @@
if not (! warned) andalso
length (new_states @ States) > ! branching_level then
(Context_Position.if_visible ctxt warning
- "Currently parsed expression could be extremely ambiguous.";
+ "Currently parsed expression could be extremely ambiguous";
warned := true)
else ();
in
--- a/src/Pure/System/isabelle_process.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Sep 01 13:45:58 2010 +0200
@@ -63,7 +63,8 @@
in
fun standard_message out_stream ch body =
- message out_stream ch (Position.properties_of (Position.thread_data ())) body;
+ message out_stream ch
+ ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
fun init_message out_stream =
message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
--- a/src/Pure/System/isar.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/System/isar.ML Wed Sep 01 13:45:58 2010 +0200
@@ -94,7 +94,10 @@
fun op >> tr =
(case Toplevel.transition true tr (state ()) of
NONE => false
- | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
+ | SOME (_, SOME exn_info) =>
+ (set_exn (SOME exn_info);
+ Toplevel.error_msg tr (ML_Compiler.exn_message (Runtime.EXCURSION_FAIL exn_info));
+ true)
| SOME (st', NONE) =>
let
val name = Toplevel.name_of tr;
--- a/src/Pure/System/session.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/System/session.scala Wed Sep 01 13:45:58 2010 +0200
@@ -190,7 +190,8 @@
result.body match {
case List(Isar_Document.Assign(id, edits)) =>
try {
- global_state.change(_.assign(id, edits))
+ val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
+ for (cmd <- cmds) command_change_buffer ! cmd
assignments.event(Session.Assignment)
}
catch { case _: Document.State.Fail => bad_result(result) }
--- a/src/Pure/Thy/thy_syntax.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Sep 01 13:45:58 2010 +0200
@@ -77,9 +77,11 @@
commands.iterator.find(_.is_unparsed) match {
case Some(first_unparsed) =>
val first =
- commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+ commands.reverse_iterator(first_unparsed).
+ dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
val last =
- commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
+ commands.iterator(first_unparsed).
+ dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
val range =
commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
--- a/src/Pure/goal.ML Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Pure/goal.ML Wed Sep 01 13:45:58 2010 +0200
@@ -159,7 +159,7 @@
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
SOME th => Drule.implies_intr_list casms
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
- | NONE => error "Tactic failed.");
+ | NONE => error "Tactic failed");
(* prove_common etc. *)
@@ -191,7 +191,7 @@
fun result () =
(case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
- NONE => err "Tactic failed."
+ NONE => err "Tactic failed"
| SOME st =>
let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
--- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 01 13:45:58 2010 +0200
@@ -190,19 +190,6 @@
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
{
- /* visible line end */
-
- // simplify slightly odd result of TextArea.getLineEndOffset
- // NB: jEdit already normalizes \r\n and \r to \n
- def visible_line_end(start: Text.Offset, end: Text.Offset): Text.Offset =
- {
- val end1 = end - 1
- if (start <= end1 && end1 < buffer.getLength &&
- buffer.getSegment(end1, 1).charAt(0) == '\n') end1
- else end
- }
-
-
/* pending text edits */
object pending_edits // owned by Swing thread
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 01 13:45:58 2010 +0200
@@ -97,6 +97,24 @@
}
+ /* visible line ranges */
+
+ // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
+ // NB: jEdit already normalizes \r\n and \r to \n
+ def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
+ {
+ val stop = if (start < end) end - 1 else end min model.buffer.getLength
+ Text.Range(start, stop)
+ }
+
+ def screen_lines_range(): Text.Range =
+ {
+ val start = text_area.getScreenLineStartOffset(0)
+ val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
+ proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
+ }
+
+
/* commands_changed_actor */
private val commands_changed_actor = actor {
@@ -106,23 +124,25 @@
val buffer = model.buffer
Isabelle.swing_buffer_lock(buffer) {
val snapshot = model.snapshot()
- if (changed.exists(snapshot.node.commands.contains)) {
- var visible_change = false
- for ((command, start) <- snapshot.node.command_starts) {
- if (changed(command)) {
- val stop = start + command.length
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(stop))
- if (line2 >= text_area.getFirstLine &&
- line1 <= text_area.getFirstLine + text_area.getVisibleLines)
- visible_change = true
- text_area.invalidateLineRange(line1, line2)
- }
- }
+
+ if (changed.exists(snapshot.node.commands.contains))
+ overview.repaint()
+
+ val visible_range = screen_lines_range()
+ val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
+ if (visible_cmds.exists(changed)) {
+ for {
+ line <- 0 until text_area.getVisibleLines
+ val start = text_area.getScreenLineStartOffset(line) if start >= 0
+ val end = text_area.getScreenLineEndOffset(line) if end >= 0
+ val range = proper_line_range(start, end)
+ val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
+ if line_cmds.exists(changed)
+ } text_area.invalidateScreenLineRange(line, line)
+
// FIXME danger of deadlock!?
- if (visible_change) model.buffer.propertiesChanged()
-
- overview.repaint() // FIXME really paint here!?
+ // FIXME potentially slow!?
+ model.buffer.propertiesChanged()
}
}
@@ -138,49 +158,26 @@
{
override def paintScreenLineRange(gfx: Graphics2D,
first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
-
- val command_range: Iterable[(Command, Text.Offset)] =
- {
- val range = snapshot.node.command_range(snapshot.revert(start(0)))
- if (range.hasNext) {
- val (cmd0, start0) = range.next
- new Iterable[(Command, Text.Offset)] {
- def iterator =
- Document.Node.command_starts(snapshot.node.commands.iterator(cmd0), start0)
- }
- }
- else Iterable.empty
- }
-
val saved_color = gfx.getColor
try {
- var y = y0
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
- val line_start = start(i)
- val line_end = model.visible_line_end(line_start, end(i))
-
- val a = snapshot.revert(line_start)
- val b = snapshot.revert(line_end)
- val cmds = command_range.iterator.
- dropWhile { case (cmd, c) => c + cmd.length <= a } .
- takeWhile { case (_, c) => c < b }
-
+ val line_range = proper_line_range(start(i), end(i))
+ val cmds = snapshot.node.command_range(snapshot.revert(line_range))
for ((command, command_start) <- cmds if !command.is_ignored) {
- val p =
- text_area.offsetToXY(line_start max snapshot.convert(command_start))
- val q =
- text_area.offsetToXY(line_end min snapshot.convert(command_start + command.length))
- if (p.y != q.y) System.err.println("Unexpected coordinates: " + p + ", " + q)
- gfx.setColor(Document_View.choose_color(snapshot, command))
- gfx.fillRect(p.x, y, q.x - p.x, line_height)
+ val range = line_range.restrict(snapshot.convert(command.range + command_start))
+ val p = text_area.offsetToXY(range.start)
+ val q = text_area.offsetToXY(range.stop)
+ if (p != null && q != null) {
+ gfx.setColor(Document_View.choose_color(snapshot, command))
+ gfx.fillRect(p.x, y + i * line_height, q.x - p.x, line_height)
+ }
}
}
- y += line_height
}
}
finally { gfx.setColor(saved_color) }
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Sep 01 11:09:50 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Sep 01 13:45:58 2010 +0200
@@ -67,12 +67,12 @@
case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
val snapshot = doc_view.model.snapshot()
val filtered_results =
- snapshot.state(cmd).results filter {
+ snapshot.state(cmd).results.iterator.map(_._2) filter {
case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
case _ => true
}
- html_panel.render(filtered_results)
+ html_panel.render(filtered_results.toList)
case _ =>
}
case None =>