--- a/src/Doc/JEdit/JEdit.thy Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Tue Apr 08 23:16:00 2014 +0200
@@ -564,13 +564,6 @@
determines an additional delay (0.0 by default), before opening a
completion popup.
- \item The system option @{system_option
- jedit_completion_dismiss_delay} determines an additional delay (0.0
- by default), before dismissing an earlier completion popup. A value
- like 0.1 is occasionally useful to reduce the chance of loosing key
- strokes when the speed of typing exceeds that of repainting GUI
- components.
-
\item The system option @{system_option jedit_completion_immediate}
(disabled by default) controls whether replacement text should be
inserted immediately without popup. This is restricted to Isabelle
--- a/src/Doc/antiquote_setup.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Doc/antiquote_setup.ML Tue Apr 08 23:16:00 2014 +0200
@@ -201,6 +201,10 @@
val _ = Context_Position.reports ctxt (map (pair pos) markup);
in true end;
+fun check_system_option ctxt (name, pos) =
+ (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
+ handle ERROR _ => false;
+
fun check_tool ctxt (name, pos) =
let
fun tool dir =
@@ -265,7 +269,7 @@
entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
entity_antiqs no_check "isatt" @{binding setting} #>
- entity_antiqs no_check "isatt" @{binding system_option} #>
+ entity_antiqs check_system_option "isatt" @{binding system_option} #>
entity_antiqs no_check "" @{binding inference} #>
entity_antiqs no_check "isatt" @{binding executable} #>
entity_antiqs check_tool "isatool" @{binding tool} #>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Tue Apr 08 23:16:00 2014 +0200
@@ -124,7 +124,7 @@
| SOME _ => (GenuineCex, Quickcheck.timings_of result)
end) ()
handle TimeLimit.TimeOut =>
- (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit}))])
+ (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
--- a/src/HOL/Prolog/prolog.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Prolog/prolog.ML Tue Apr 08 23:16:00 2014 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-Options.default_put_bool @{option show_main_goal} true;
+Options.default_put_bool @{system_option show_main_goal} true;
structure Prolog =
struct
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Apr 08 23:16:00 2014 +0200
@@ -285,7 +285,7 @@
type tptp_problem = tptp_line list
-fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
fun nameof_tff_atom_type (Atom_type str) = str
| nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Apr 08 23:16:00 2014 +0200
@@ -42,7 +42,7 @@
ML {*
if test_all @{context} then ()
else
- (Options.default_put_bool @{option ML_exception_trace} true;
+ (Options.default_put_bool @{system_option ML_exception_trace} true;
default_print_depth 200; (* FIXME proper ML_print_depth within context!? *)
PolyML.Compiler.maxInlineSize := 0)
*}
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Tue Apr 08 23:16:00 2014 +0200
@@ -34,7 +34,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_nitpick}
+ @{system_option auto_nitpick}
"auto-nitpick"
"Run Nitpick automatically"
@@ -396,6 +396,6 @@
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
-val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
+val _ = Try.tool_setup (nitpickN, (50, @{system_option auto_nitpick}, try_nitpick))
end;
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Tue Apr 08 23:16:00 2014 +0200
@@ -100,7 +100,7 @@
fun z3_non_commercial () =
let
- val flag1 = Options.default_string @{option z3_non_commercial}
+ val flag1 = Options.default_string @{system_option z3_non_commercial}
val flag2 = getenv "Z3_NON_COMMERCIAL"
in
if accepted flag1 then Z3_Non_Commercial_Accepted
--- a/src/HOL/Tools/SMT2/smt2_systems.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML Tue Apr 08 23:16:00 2014 +0200
@@ -97,7 +97,7 @@
fun z3_non_commercial () =
let
- val flag1 = Options.default_string @{option z3_non_commercial}
+ val flag1 = Options.default_string @{system_option z3_non_commercial}
val flag2 = getenv "Z3_NON_COMMERCIAL"
in
if accepted flag1 then Z3_Non_Commercial_Accepted
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Apr 08 23:16:00 2014 +0200
@@ -43,7 +43,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_sledgehammer}
+ @{system_option auto_sledgehammer}
"auto-sledgehammer"
"Run Sledgehammer automatically"
@@ -72,7 +72,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_proof
NONE
- @{option sledgehammer_timeout}
+ @{system_option sledgehammer_timeout}
"Sledgehammer: Time Limit"
"ATPs will be interrupted after this time (in seconds)"
@@ -229,7 +229,7 @@
|> fold (AList.default (op =))
[("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
("timeout",
- let val timeout = Options.default_int @{option sledgehammer_timeout} in
+ let val timeout = Options.default_int @{system_option sledgehammer_timeout} in
[if timeout <= 0 then "none" else string_of_int timeout]
end)]
end
@@ -472,7 +472,7 @@
state
end
-val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
val _ =
Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
--- a/src/HOL/Tools/try0.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/try0.ML Tue Apr 08 23:16:00 2014 +0200
@@ -25,7 +25,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_methods}
+ @{system_option auto_methods}
"auto-try0"
"Try standard proof methods";
@@ -193,6 +193,6 @@
fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
-val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0));
+val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
end;
--- a/src/Pure/General/position.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/General/position.ML Tue Apr 08 23:16:00 2014 +0200
@@ -35,6 +35,7 @@
val default_properties: T -> Properties.T -> Properties.T
val markup: T -> Markup.T -> Markup.T
val is_reported: T -> bool
+ val is_reported_range: T -> bool
val reported_text: T -> Markup.T -> string -> string
val report_text: T -> Markup.T -> string -> unit
val report: T -> Markup.T -> unit
@@ -166,6 +167,7 @@
(* reports *)
fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
fun report_text pos markup txt = Output.report [reported_text pos markup txt];
--- a/src/Pure/General/position.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/General/position.scala Tue Apr 08 23:16:00 2014 +0200
@@ -30,6 +30,10 @@
object Line_File
{
+ def apply(line: Int, file: String): T =
+ (if (line > 0) Line(line) else Nil) :::
+ (if (file != "") File(file) else Nil)
+
def unapply(pos: T): Option[(Int, String)] =
(pos, pos) match {
case (Line(i), File(name)) => Some((i, name))
@@ -79,10 +83,15 @@
object Reported
{
- def unapply(pos: T): Option[(Long, String, Symbol.Range)] =
+ def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
(pos, pos) match {
case (Id(id), Range(range)) =>
- Some((id, File.unapply(pos).getOrElse(""), range))
+ val chunk_name =
+ pos match {
+ case File(name) => Text.Chunk.File(name)
+ case _ => Text.Chunk.Default
+ }
+ Some((id, chunk_name, range))
case _ => None
}
}
--- a/src/Pure/General/symbol.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/General/symbol.scala Tue Apr 08 23:16:00 2014 +0200
@@ -125,16 +125,14 @@
object Index
{
- def apply(text: CharSequence): Index = new Index(text)
- }
+ private sealed case class Entry(chr: Int, sym: Int)
- final class Index private(text: CharSequence)
- {
- private sealed case class Entry(chr: Int, sym: Int)
- private val index: Array[Entry] =
+ val empty: Index = new Index(Nil)
+
+ def apply(text: CharSequence): Index =
{
val matcher = new Matcher(text)
- val buf = new mutable.ArrayBuffer[Entry]
+ val buf = new mutable.ListBuffer[Entry]
var chr = 0
var sym = 0
while (chr < text.length) {
@@ -143,8 +141,14 @@
sym += 1
if (n > 1) buf += Entry(chr, sym)
}
- buf.toArray
+ if (buf.isEmpty) empty else new Index(buf.toList)
}
+ }
+
+ final class Index private(entries: List[Index.Entry])
+ {
+ private val hash: Int = entries.hashCode
+ private val index: Array[Index.Entry] = entries.toArray
def decode(symbol_offset: Offset): Text.Offset =
{
@@ -166,7 +170,6 @@
}
def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
- private val hash: Int = index.toList.hashCode
override def hashCode: Int = hash
override def equals(that: Any): Boolean =
that match {
--- a/src/Pure/Isar/isar_syn.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Apr 08 23:16:00 2014 +0200
@@ -984,7 +984,7 @@
(opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
Toplevel.keep (fn state =>
(if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
- case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
+ case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
Toplevel.quiet := false;
Print_Mode.with_modes modes (Toplevel.print_state true) state))));
--- a/src/Pure/Isar/parse.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Isar/parse.scala Tue Apr 08 23:16:00 2014 +0200
@@ -25,31 +25,37 @@
if (!filter_proper || in.atEnd || in.first.is_proper) in
else proper(in.rest)
- def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
- {
- def apply(raw_input: Input) =
- {
- val in = proper(raw_input)
- if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
- else {
- val token = in.first
- if (pred(token)) Success(token, proper(in.rest))
- else
- token.text match {
- case (txt, "") =>
- Failure(s + " expected,\nbut " + txt + " was found", in)
- case (txt1, txt2) =>
- Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
- }
+ def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
+ new Parser[(Elem, Token.Pos)] {
+ def apply(raw_input: Input) =
+ {
+ val in = proper(raw_input)
+ if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
+ else {
+ val pos =
+ in.pos match {
+ case pos: Token.Pos => pos
+ case _ => Token.Pos.none
+ }
+ val token = in.first
+ if (pred(token)) Success((token, pos), proper(in.rest))
+ else
+ token.text match {
+ case (txt, "") =>
+ Failure(s + " expected,\nbut " + txt + " was found", in)
+ case (txt1, txt2) =>
+ Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
+ }
+ }
}
}
- }
def atom(s: String, pred: Elem => Boolean): Parser[String] =
- token(s, pred) ^^ (_.content)
+ token(s, pred) ^^ { case (tok, _) => tok.content }
- def command(name: String): Parser[String] =
- atom("command " + quote(name), tok => tok.is_command && tok.source == name)
+ def command(name: String): Parser[Position.T] =
+ token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
+ { case (_, pos) => pos.position }
def keyword(name: String): Parser[String] =
atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
--- a/src/Pure/Isar/token.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Isar/token.scala Tue Apr 08 23:16:00 2014 +0200
@@ -121,25 +121,31 @@
/* token reader */
- class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position
+ object Pos
+ {
+ val none: Pos = new Pos(0, "")
+ }
+
+ final class Pos private[Token](val line: Int, val file: String)
+ extends scala.util.parsing.input.Position
{
def column = 0
def lineContents = ""
- override def toString =
- if (file == "") ("line " + line.toString)
- else ("line " + line.toString + " of " + quote(file))
- def advance(token: Token): Position =
+ def advance(token: Token): Pos =
{
var n = 0
for (c <- token.content if c == '\n') n += 1
- if (n == 0) this else new Position(line + n, file)
+ if (n == 0) this else new Pos(line + n, file)
}
+
+ def position: Position.T = Position.Line_File(line, file)
+ override def toString: String = Position.here(position)
}
abstract class Reader extends scala.util.parsing.input.Reader[Token]
- private class Token_Reader(tokens: List[Token], val pos: Position) extends Reader
+ private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
{
def first = tokens.head
def rest = new Token_Reader(tokens.tail, pos.advance(first))
@@ -147,7 +153,7 @@
}
def reader(tokens: List[Token], file: String = ""): Reader =
- new Token_Reader(tokens, new Position(1, file))
+ new Token_Reader(tokens, new Pos(1, file))
}
--- a/src/Pure/ML/ml_antiquotations.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Tue Apr 08 23:16:00 2014 +0200
@@ -8,9 +8,10 @@
struct
val _ = Theory.setup
- (ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
- (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
- ML_Syntax.print_string name))) #>
+ (ML_Antiquotation.value @{binding system_option}
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos (Options.default_markup (name, pos));
+ ML_Syntax.print_string name))) #>
ML_Antiquotation.value @{binding theory}
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
--- a/src/Pure/ML/ml_lex.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/ML/ml_lex.ML Tue Apr 08 23:16:00 2014 +0200
@@ -325,8 +325,12 @@
val read = gen_read false;
fun read_source SML {delimited, text, pos} =
- (Position.report pos ((if SML then Markup.language_SML else Markup.language_ML) delimited);
- gen_read SML pos text);
+ let
+ val language = if SML then Markup.language_SML else Markup.language_ML;
+ val _ =
+ if Position.is_reported_range pos then Position.report pos (language delimited)
+ else ();
+ in gen_read SML pos text end;
end;
--- a/src/Pure/PIDE/command.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/command.ML Tue Apr 08 23:16:00 2014 +0200
@@ -6,7 +6,7 @@
signature COMMAND =
sig
- type blob = (string * string * (SHA1.digest * string list) option) Exn.result
+ type blob = (string * (SHA1.digest * string list) option) Exn.result
val read_file: Path.T -> Position.T -> Path.T -> Token.file
val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
type eval
@@ -87,7 +87,7 @@
(* read *)
type blob =
- (string * string * (SHA1.digest * string list) option) Exn.result; (*file, path, digest, lines*)
+ (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*)
fun read_file master_dir pos src_path =
let
@@ -115,16 +115,16 @@
[span] => span
|> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
let
- fun make_file src_path (Exn.Res (_, _, NONE)) =
+ fun make_file src_path (Exn.Res (_, NONE)) =
Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
- | make_file src_path (Exn.Res (file_node, file_path, SOME (digest, lines))) =
- (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_path)];
+ | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
+ (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
Exn.Res (blob_file src_path lines digest file_node))
| make_file _ (Exn.Exn e) = Exn.Exn e;
val src_paths = Keyword.command_files cmd path;
in
if null blobs then
- map2 make_file src_paths (map (K (Exn.Res ("", "", NONE))) src_paths)
+ map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
else if length src_paths = length blobs then
map2 make_file src_paths blobs
else error ("Misalignment of inlined files" ^ Position.here pos)
--- a/src/Pure/PIDE/command.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/command.scala Tue Apr 08 23:16:00 2014 +0200
@@ -15,7 +15,7 @@
object Command
{
type Edit = (Option[Command], Option[Command])
- type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
+ type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
@@ -60,10 +60,10 @@
object Markup_Index
{
- val markup: Markup_Index = Markup_Index(false, "")
+ val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
}
- sealed case class Markup_Index(status: Boolean, file_name: String)
+ sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
object Markups
{
@@ -81,6 +81,17 @@
def add(index: Markup_Index, markup: Text.Markup): Markups =
new Markups(rep + (index -> (this(index) + markup)))
+ def redirection_iterator: Iterator[Document_ID.Generic] =
+ for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
+ yield id
+
+ def redirect(other_id: Document_ID.Generic): Markups =
+ new Markups(
+ (for {
+ (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
+ if other_id == id
+ } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
+
override def hashCode: Int = rep.hashCode
override def equals(that: Any): Boolean =
that match {
@@ -124,6 +135,9 @@
def markup(index: Markup_Index): Markup_Tree = markups(index)
+ def redirect(other_command: Command): State =
+ new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
+
def eq_content(other: State): Boolean =
command.source == other.command.source &&
@@ -134,16 +148,19 @@
private def add_status(st: Markup): State =
copy(status = st :: status)
- private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
+ private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
{
val markups1 =
if (status || Protocol.liberal_status_elements(m.info.name))
- markups.add(Markup_Index(true, file_name), m)
+ markups.add(Markup_Index(true, chunk_name), m)
else markups
- copy(markups = markups1.add(Markup_Index(false, file_name), m))
+ copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
}
- def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
+ def accumulate(
+ self_id: Document_ID.Generic => Boolean,
+ other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
+ message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -151,7 +168,7 @@
case elem @ XML.Elem(markup, Nil) =>
state.
add_status(markup).
- add_markup(true, "", Text.Info(command.proper_range, elem))
+ add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
case _ =>
System.err.println("Ignored status message: " + msg)
state
@@ -163,19 +180,31 @@
def bad(): Unit = System.err.println("Ignored report message: " + msg)
msg match {
- case XML.Elem(Markup(name,
- atts @ Position.Reported(id, file_name, symbol_range)), args)
- if valid_id(id) =>
- command.chunks.get(file_name) match {
- case Some(chunk) =>
- chunk.incorporate(symbol_range) match {
+ case XML.Elem(
+ Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
+
+ val target =
+ if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
+ Some((chunk_name, command.chunks(chunk_name)))
+ else if (chunk_name == Text.Chunk.Default) other_id(id)
+ else None
+
+ target match {
+ case Some((target_name, target_chunk)) =>
+ target_chunk.incorporate(symbol_range) match {
case Some(range) =>
val props = Position.purge(atts)
val info = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(false, file_name, info)
+ state.add_markup(false, target_name, info)
case None => bad(); state
}
- case None => bad(); state
+ case None =>
+ chunk_name match {
+ // FIXME workaround for static positions stemming from batch build
+ case Text.Chunk.File(name) if name.endsWith(".thy") =>
+ case _ => bad()
+ }
+ state
}
case XML.Elem(Markup(name, atts), args)
@@ -183,9 +212,9 @@
val range = command.proper_range
val props = Position.purge(atts)
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
- state.add_markup(false, "", info)
+ state.add_markup(false, Text.Chunk.Default, info)
- case _ => /* FIXME bad(); */ state
+ case _ => bad(); state
}
})
case XML.Elem(Markup(name, props), body) =>
@@ -197,9 +226,9 @@
var st = copy(results = results + (i -> message1))
if (Protocol.is_inlined(message)) {
for {
- (file_name, chunk) <- command.chunks
- range <- Protocol.message_positions(valid_id, chunk, message)
- } st = st.add_markup(false, file_name, Text.Info(range, message2))
+ (chunk_name, chunk) <- command.chunks.iterator
+ range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
+ } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
}
st
@@ -214,49 +243,6 @@
/** static content **/
- /* text chunks */
-
- abstract class Chunk
- {
- def file_name: String
- def length: Int
- def range: Text.Range
- def decode(symbol_range: Symbol.Range): Text.Range
-
- def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
- {
- def inc(r: Symbol.Range): Option[Text.Range] =
- range.try_restrict(decode(r)) match {
- case Some(r1) if !r1.is_singularity => Some(r1)
- case _ => None
- }
- inc(symbol_range) orElse inc(symbol_range - 1)
- }
- }
-
- // file name and position information, *without* persistent text
- class File(val file_name: String, text: CharSequence) extends Chunk
- {
- val length = text.length
- val range = Text.Range(0, length)
- private val symbol_index = Symbol.Index(text)
- def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
-
- private val hash: Int = (file_name, length, symbol_index).hashCode
- override def hashCode: Int = hash
- override def equals(that: Any): Boolean =
- that match {
- case other: File =>
- hash == other.hash &&
- file_name == other.file_name &&
- length == other.length &&
- symbol_index == other.symbol_index
- case _ => false
- }
- override def toString: String = "Command.File(" + file_name + ")"
- }
-
-
/* make commands */
def name(span: List[Token]): String =
@@ -344,7 +330,6 @@
val source: String,
val init_results: Command.Results,
val init_markup: Markup_Tree)
- extends Command.Chunk
{
/* classification */
@@ -373,27 +358,24 @@
def blobs_digests: List[SHA1.Digest] =
for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
- val chunks: Map[String, Command.Chunk] =
- (("" -> this) ::
- (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap
+
+ /* source chunks */
+
+ val chunk: Text.Chunk = Text.Chunk(source)
-
- /* source */
-
- def file_name: String = ""
+ val chunks: Map[Text.Chunk.Name, Text.Chunk] =
+ ((Text.Chunk.Default -> chunk) ::
+ (for (Exn.Res((name, Some((_, file)))) <- blobs)
+ yield (Text.Chunk.File(name.node) -> file))).toMap
def length: Int = source.length
- val range: Text.Range = Text.Range(0, length)
+ def range: Text.Range = chunk.range
val proper_range: Text.Range =
Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
def source(range: Text.Range): String = source.substring(range.start, range.stop)
- private lazy val symbol_index = Symbol.Index(source)
- def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
- def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
-
/* accumulated results */
--- a/src/Pure/PIDE/document.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/document.ML Tue Apr 08 23:16:00 2014 +0200
@@ -18,7 +18,7 @@
type state
val init_state: state
val define_blob: string -> string -> state -> state
- type blob_digest = (string * string * string option) Exn.result
+ type blob_digest = (string * string option) Exn.result
val define_command: Document_ID.command -> string -> blob_digest list -> string ->
state -> state
val remove_versions: Document_ID.version list -> state -> state
@@ -219,8 +219,7 @@
(** main state -- document structure and execution process **)
-type blob_digest =
- (string * string * string option) Exn.result; (* file node name, path, raw digest*)
+type blob_digest = (string * string option) Exn.result; (*file node name, raw digest*)
type execution =
{version_id: Document_ID.version, (*static version id*)
@@ -293,8 +292,8 @@
| SOME content => content);
fun resolve_blob state (blob_digest: blob_digest) =
- blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
- (file, path, Option.map (the_blob state) raw_digest));
+ blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
+ (file_node, Option.map (the_blob state) raw_digest));
(* commands *)
@@ -343,7 +342,7 @@
val blobs' =
(commands', Symtab.empty) |->
Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
- fold (fn Exn.Res (_, _, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
+ fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
in (versions', blobs', commands', execution) end);
--- a/src/Pure/PIDE/document.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/document.scala Tue Apr 08 23:16:00 2014 +0200
@@ -45,7 +45,7 @@
/* document blobs: auxiliary files */
- sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+ sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
{
def unchanged: Blob = copy(changed = false)
}
@@ -483,11 +483,19 @@
}
final case class State private(
+ /*reachable versions*/
val versions: Map[Document_ID.Version, Version] = Map.empty,
- val blobs: Set[SHA1.Digest] = Set.empty, // inlined files
- val commands: Map[Document_ID.Command, Command.State] = Map.empty, // static markup from define_command
- val execs: Map[Document_ID.Exec, Command.State] = Map.empty, // dynamic markup from execution
+ /*inlined auxiliary files*/
+ val blobs: Set[SHA1.Digest] = Set.empty,
+ /*static markup from define_command*/
+ val commands: Map[Document_ID.Command, Command.State] = Map.empty,
+ /*dynamic markup from execution*/
+ val execs: Map[Document_ID.Exec, Command.State] = Map.empty,
+ /*command-exec assignment for each version*/
val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
+ /*commands with markup produced by other commands (imm_succs)*/
+ val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
+ /*explicit (linear) history*/
val history: History = History.init)
{
private def fail[A]: A = throw new State.Fail(this)
@@ -524,23 +532,35 @@
def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
- def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
+ private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
id == st.command.id ||
(execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
+ private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
+ (execs.get(id) orElse commands.get(id)).map(st =>
+ ((Text.Chunk.Id(st.command.id), st.command.chunk)))
+
+ private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
+ (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
+ graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
+
def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
+ {
execs.get(id) match {
case Some(st) =>
- val new_st = st + (valid_id(st), message)
- (new_st, copy(execs = execs + (id -> new_st)))
+ val new_st = st.accumulate(self_id(st), other_id _, message)
+ val execs1 = execs + (id -> new_st)
+ (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
case None =>
commands.get(id) match {
case Some(st) =>
- val new_st = st + (valid_id(st), message)
- (new_st, copy(commands = commands + (id -> new_st)))
+ val new_st = st.accumulate(self_id(st), other_id _, message)
+ val commands1 = commands + (id -> new_st)
+ (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
case None => fail
}
}
+ }
def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
{
@@ -629,27 +649,48 @@
execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
}
}
- copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
+ copy(
+ versions = versions1,
+ blobs = blobs1,
+ commands = commands1,
+ execs = execs1,
+ commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
assignments = assignments1)
}
- def command_states(version: Version, command: Command): List[Command.State] =
+ private def command_states_self(version: Version, command: Command)
+ : List[(Document_ID.Generic, Command.State)] =
{
require(is_assigned(version))
try {
the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
- .map(the_dynamic_state(_)) match {
+ .map(id => id -> the_dynamic_state(id)) match {
case Nil => fail
- case states => states
+ case res => res
}
}
catch {
case _: State.Fail =>
- try { List(the_static_state(command.id)) }
- catch { case _: State.Fail => List(command.init_state) }
+ try { List(command.id -> the_static_state(command.id)) }
+ catch { case _: State.Fail => List(command.id -> command.init_state) }
}
}
+ def command_states(version: Version, command: Command): List[Command.State] =
+ {
+ val self = command_states_self(version, command)
+ val others =
+ if (commands_redirection.defined(command.id)) {
+ (for {
+ command_id <- commands_redirection.imm_succs(command.id).iterator
+ (id, st) <- command_states_self(version, the_static_state(command_id).command)
+ if !self.exists(_._1 == id)
+ } yield (id, st)).toMap.valuesIterator.toList
+ }
+ else Nil
+ self.map(_._2) ::: others.map(_.redirect(command))
+ }
+
def command_results(version: Version, command: Command): Command.Results =
Command.State.merge_results(command_states(version, command))
@@ -731,15 +772,15 @@
status: Boolean = false): List[Text.Info[A]] =
{
val former_range = revert(range)
- val (file_name, command_iterator) =
+ val (chunk_name, command_iterator) =
load_commands match {
- case command :: _ => (node_name.node, Iterator((command, 0)))
- case _ => ("", node.command_iterator(former_range))
+ case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
+ case _ => (Text.Chunk.Default, node.command_iterator(former_range))
}
- val markup_index = Command.Markup_Index(status, file_name)
+ val markup_index = Command.Markup_Index(status, chunk_name)
(for {
(command, command_start) <- command_iterator
- chunk <- command.chunks.get(file_name).iterator
+ chunk <- command.chunks.get(chunk_name).iterator
states = state.command_states(version, command)
res = result(states)
range = (former_range - command_start).restrict(chunk.range)
--- a/src/Pure/PIDE/markup.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/markup.ML Tue Apr 08 23:16:00 2014 +0200
@@ -63,6 +63,7 @@
val fbreakN: string val fbreak: T
val itemN: string val item: T
val hiddenN: string val hidden: T
+ val system_optionN: string
val theoryN: string
val classN: string
val type_nameN: string
@@ -358,7 +359,9 @@
val (hiddenN, hidden) = markup_elem "hidden";
-(* logical entities *)
+(* formal entities *)
+
+val system_optionN = "system_option";
val theoryN = "theory";
val classN = "class";
--- a/src/Pure/PIDE/protocol.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML Tue Apr 08 23:16:00 2014 +0200
@@ -34,7 +34,7 @@
YXML.parse_body blobs_yxml |>
let open XML.Decode in
list (variant
- [fn ([], a) => Exn.Res (triple string string (option string) a),
+ [fn ([], a) => Exn.Res (pair string (option string) a),
fn ([], a) => Exn.Exn (ERROR (string a))])
end;
in
--- a/src/Pure/PIDE/protocol.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Apr 08 23:16:00 2014 +0200
@@ -95,9 +95,9 @@
def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
def is_running: Boolean = runs != 0
+ def is_warned: Boolean = warned
+ def is_failed: Boolean = failed
def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
- def is_warned: Boolean = is_finished && warned
- def is_failed: Boolean = failed
}
val proper_status_elements =
@@ -127,9 +127,9 @@
/* node status */
sealed case class Node_Status(
- unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
+ unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int)
{
- def total: Int = unprocessed + running + finished + warned + failed
+ def total: Int = unprocessed + running + warned + failed + finished
}
def node_status(
@@ -137,20 +137,20 @@
{
var unprocessed = 0
var running = 0
- var finished = 0
var warned = 0
var failed = 0
+ var finished = 0
for (command <- node.commands.iterator) {
val states = state.command_states(version, command)
val status = Status.merge(states.iterator.map(_.protocol_status))
if (status.is_running) running += 1
else if (status.is_warned) warned += 1
+ else if (status.is_failed) failed += 1
else if (status.is_finished) finished += 1
- else if (status.is_failed) failed += 1
else unprocessed += 1
}
- Node_Status(unprocessed, running, finished, warned, failed)
+ Node_Status(unprocessed, running, warned, failed, finished)
}
@@ -301,14 +301,15 @@
Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(
- valid_id: Document_ID.Generic => Boolean,
- chunk: Command.Chunk,
+ self_id: Document_ID.Generic => Boolean,
+ chunk_name: Text.Chunk.Name,
+ chunk: Text.Chunk,
message: XML.Elem): Set[Text.Range] =
{
def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
props match {
- case Position.Reported(id, file_name, symbol_range)
- if valid_id(id) && file_name == chunk.file_name =>
+ case Position.Reported(id, name, symbol_range)
+ if self_id(id) && name == chunk_name =>
chunk.incorporate(symbol_range) match {
case Some(range) => set + range
case _ => set
@@ -352,8 +353,7 @@
val encode_blob: T[Command.Blob] =
variant(List(
{ case Exn.Res((a, b)) =>
- (Nil, triple(string, string, option(string))(
- (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
+ (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
YXML.string_of_body(list(encode_blob)(command.blobs))
}
--- a/src/Pure/PIDE/text.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/text.scala Tue Apr 08 23:16:00 2014 +0200
@@ -71,6 +71,44 @@
}
+ /* named chunks with sparse symbol index */
+
+ object Chunk
+ {
+ sealed abstract class Name
+ case object Default extends Name
+ case class Id(id: Document_ID.Generic) extends Name
+ case class File(name: String) extends Name
+
+ def apply(text: CharSequence): Chunk =
+ new Chunk(Range(0, text.length), Symbol.Index(text))
+ }
+
+ final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
+ {
+ override def hashCode: Int = (range, symbol_index).hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Chunk =>
+ range == other.range &&
+ symbol_index == other.symbol_index
+ case _ => false
+ }
+
+ def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
+ def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
+ def incorporate(symbol_range: Symbol.Range): Option[Range] =
+ {
+ def in(r: Symbol.Range): Option[Range] =
+ range.try_restrict(decode(r)) match {
+ case Some(r1) if !r1.is_singularity => Some(r1)
+ case _ => None
+ }
+ in(symbol_range) orElse in(symbol_range - 1)
+ }
+ }
+
+
/* perspective */
object Perspective
--- a/src/Pure/System/isabelle_system.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Apr 08 23:16:00 2014 +0200
@@ -10,8 +10,9 @@
import java.util.regex.Pattern
import java.io.{File => JFile, BufferedReader, InputStreamReader,
- BufferedWriter, OutputStreamWriter}
-import java.nio.file.Files
+ BufferedWriter, OutputStreamWriter, IOException}
+import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, URLDecoder, MalformedURLException}
import scala.util.matching.Regex
@@ -104,7 +105,7 @@
shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
if (rc != 0) error(output)
-
+
val entries =
(for (entry <- File.read(dump) split "\0" if entry != "") yield {
val i = entry.indexOf('=')
@@ -394,6 +395,47 @@
}
+ /* tmp dirs */
+
+ def rm_tree(root: JFile)
+ {
+ root.delete
+ if (root.isDirectory) {
+ Files.walkFileTree(root.toPath,
+ new SimpleFileVisitor[JPath] {
+ override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
+ {
+ Files.delete(file)
+ FileVisitResult.CONTINUE
+ }
+
+ override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
+ {
+ if (e == null) {
+ Files.delete(dir)
+ FileVisitResult.CONTINUE
+ }
+ else throw e
+ }
+ }
+ )
+ }
+ }
+
+ def tmp_dir(name: String): JFile =
+ {
+ val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
+ dir.deleteOnExit
+ dir
+ }
+
+ def with_tmp_dir[A](name: String)(body: JFile => A): A =
+ {
+ val dir = tmp_dir(name)
+ try { body(dir) } finally { rm_tree(dir) }
+ }
+
+
/* bash */
final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
@@ -444,35 +486,6 @@
def bash(script: String): Bash_Result = bash_env(null, null, script)
- /* tmp dirs */
-
- private def system_command(cmd: String)
- {
- val res = bash(cmd)
- if (res.rc != 0)
- error(cat_lines(("System command failed: " + cmd) :: res.out_lines ::: res.err_lines))
- }
-
- def rm_tree(dir: JFile)
- {
- dir.delete
- if (dir.isDirectory) system_command("rm -r -f " + shell_path(dir))
- }
-
- def tmp_dir(name: String): JFile =
- {
- val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
- dir.deleteOnExit
- dir
- }
-
- def with_tmp_dir[A](name: String)(body: JFile => A): A =
- {
- val dir = tmp_dir(name)
- try { body(dir) } finally { rm_tree(dir) }
- }
-
-
/* system tools */
def isabelle_tool(name: String, args: String*): (String, Int) =
--- a/src/Pure/System/options.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/System/options.ML Tue Apr 08 23:16:00 2014 +0200
@@ -13,6 +13,7 @@
val unknownT: string
type T
val empty: T
+ val markup: T -> string * Position.T -> Markup.T
val typ: T -> string -> string
val bool: T -> string -> bool
val int: T -> string -> int
@@ -22,10 +23,11 @@
val put_int: string -> int -> T -> T
val put_real: string -> real -> T -> T
val put_string: string -> string -> T -> T
- val declare: {name: string, typ: string, value: string} -> T -> T
+ val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T
val update: string -> string -> T -> T
val decode: XML.body -> T
val default: unit -> T
+ val default_markup: string * Position.T -> Markup.T
val default_typ: string -> string
val default_bool: string -> bool
val default_int: string -> int
@@ -53,7 +55,7 @@
val stringT = "string";
val unknownT = "unknown";
-datatype T = Options of {typ: string, value: string} Symtab.table;
+datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table;
val empty = Options Symtab.empty;
@@ -73,6 +75,17 @@
end;
+(* markup *)
+
+fun markup options (name, pos) =
+ let
+ val opt =
+ check_name options name
+ handle ERROR msg => error (msg ^ Position.here pos);
+ val props = Position.def_properties_of (#pos opt);
+ in Markup.properties props (Markup.entity Markup.system_optionN name) end;
+
+
(* typ *)
fun typ options name = #typ (check_name options name);
@@ -82,7 +95,7 @@
fun put T print name x (options as Options tab) =
let val opt = check_type options name T
- in Options (Symtab.update (name, {typ = #typ opt, value = print x}) tab) end;
+ in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end;
fun get T parse options name =
let val opt = check_type options name T in
@@ -118,29 +131,39 @@
else ()
end;
-fun declare {name, typ, value} (Options tab) =
+fun declare {pos, name, typ, value} (Options tab) =
let
- val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
- handle Symtab.DUP _ => error ("Duplicate declaration of system option " ^ quote name);
+ val options' =
+ (case Symtab.lookup tab name of
+ SOME other =>
+ error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^
+ Position.here (#pos other))
+ | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab));
val _ =
typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse
- error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ);
+ error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^
+ Position.here pos);
val _ = check_value options' name;
in options' end;
fun update name value (options as Options tab) =
let
val opt = check_name options name;
- val options' = Options (Symtab.update (name, {typ = #typ opt, value = value}) tab);
+ val options' =
+ Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab);
val _ = check_value options' name;
in options' end;
(* decode *)
-fun decode body =
- fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
- (let open XML.Decode in list (triple string string string) end body) empty;
+fun decode_opt body =
+ let open XML.Decode
+ in list (pair properties (pair string (pair string string))) end body
+ |> map (fn (props, (name, (typ, value))) =>
+ {pos = Position.of_properties props, name = name, typ = typ, value = value});
+
+fun decode body = fold declare (decode_opt body) empty;
@@ -160,6 +183,7 @@
SOME options => options
| NONE => err_no_default ());
+fun default_markup arg = markup (default ()) arg;
fun default_typ name = typ (default ()) name;
fun default_bool name = bool (default ()) name;
fun default_int name = int (default ()) name;
--- a/src/Pure/System/options.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/System/options.scala Tue Apr 08 23:16:00 2014 +0200
@@ -29,8 +29,15 @@
case object String extends Type
case object Unknown extends Type
- case class Opt(public: Boolean, name: String, typ: Type, value: String, default_value: String,
- description: String, section: String)
+ case class Opt(
+ public: Boolean,
+ pos: Position.T,
+ name: String,
+ typ: Type,
+ value: String,
+ default_value: String,
+ description: String,
+ section: String)
{
private def print(default: Boolean): String =
{
@@ -88,8 +95,8 @@
{ case _ ~ a => (options: Options) => options.set_section(a) } |
opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
- { case a ~ _ ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
- (options: Options) => options.declare(a.isDefined, b, c, d, e) }
+ { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+ (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
}
val prefs_entry: Parser[Options => Options] =
@@ -260,11 +267,18 @@
}
}
- def declare(public: Boolean, name: String, typ_name: String, value: String, description: String)
- : Options =
+ def declare(
+ public: Boolean,
+ pos: Position.T,
+ name: String,
+ typ_name: String,
+ value: String,
+ description: String): Options =
{
options.get(name) match {
- case Some(_) => error("Duplicate declaration of option " + quote(name))
+ case Some(other) =>
+ error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
+ Position.here(other.pos))
case None =>
val typ =
typ_name match {
@@ -272,9 +286,11 @@
case "int" => Options.Int
case "real" => Options.Real
case "string" => Options.String
- case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
+ case _ =>
+ error("Unknown type for option " + quote(name) + " : " + quote(typ_name) +
+ Position.here(pos))
}
- val opt = Options.Opt(public, name, typ, value, value, description, section)
+ val opt = Options.Opt(public, pos, name, typ, value, value, description, section)
(new Options(options + (name -> opt), section)).check_value(name)
}
}
@@ -282,10 +298,10 @@
def add_permissive(name: String, value: String): Options =
{
if (options.isDefinedAt(name)) this + (name, value)
- else
- new Options(
- options +
- (name -> Options.Opt(false, name, Options.Unknown, value, value, "", "")), section)
+ else {
+ val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "")
+ new Options(options + (name -> opt), section)
+ }
}
def + (name: String, value: String): Options =
@@ -330,11 +346,11 @@
def encode: XML.Body =
{
val opts =
- for ((name, opt) <- options.toList; if !opt.unknown)
- yield (name, opt.typ.print, opt.value)
+ for ((_, opt) <- options.toList; if !opt.unknown)
+ yield (opt.pos, (opt.name, (opt.typ.print, opt.value)))
- import XML.Encode.{string => str, _}
- list(triple(str, str, str))(opts)
+ import XML.Encode.{string => string_, _}
+ list(pair(properties, pair(string_, pair(string_, string_))))(opts)
}
--- a/src/Pure/Thy/thy_syntax.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Tue Apr 08 23:16:00 2014 +0200
@@ -271,7 +271,7 @@
Exn.capture {
val name =
Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
- val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
+ val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
(name, blob)
})
}
--- a/src/Pure/Tools/build.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Tools/build.scala Tue Apr 08 23:16:00 2014 +0200
@@ -203,16 +203,14 @@
private object Parser extends Parse.Parser
{
- def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
-
- def chapter(pos: Position.T): Parser[Chapter] =
+ val chapter: Parser[Chapter] =
{
val chapter_name = atom("chapter name", _.is_name)
command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
}
- def session_entry(pos: Position.T): Parser[Session_Entry] =
+ val session_entry: Parser[Session_Entry] =
{
val session_name = atom("session name", _.is_name)
@@ -234,7 +232,7 @@
((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
rep1(theories) ~
((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
- { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
+ { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
Session_Entry(pos, a, b, c, d, e, f, g, h) }
}
@@ -242,7 +240,7 @@
{
val toks = root_syntax.scan(File.read(root))
- parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
+ parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
case Success(result, _) =>
var chapter = chapter_default
val entries = new mutable.ListBuffer[(String, Session_Entry)]
--- a/src/Pure/Tools/find_theorems.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML Tue Apr 08 23:16:00 2014 +0200
@@ -206,7 +206,7 @@
val goal' = Thm.transfer thy' goal;
fun limited_etac thm i =
- Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
+ Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
fun try_thm thm =
if Thm.no_prems thm then rtac thm 1 goal'
else
@@ -405,7 +405,7 @@
else raw_matches;
val len = length matches;
- val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
+ val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
val find =
--- a/src/Pure/Tools/proof_general_pure.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML Tue Apr 08 23:16:00 2014 +0200
@@ -17,49 +17,49 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_types}
+ @{system_option show_types}
"show-types"
"Include types in display of Isabelle terms";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_sorts}
+ @{system_option show_sorts}
"show-sorts"
"Include sorts in display of Isabelle types";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_consts}
+ @{system_option show_consts}
"show-consts"
"Show types of consts in Isabelle goal display";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option names_long}
+ @{system_option names_long}
"long-names"
"Show fully qualified names in Isabelle terms";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_brackets}
+ @{system_option show_brackets}
"show-brackets"
"Show full bracketing in Isabelle terms";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option show_main_goal}
+ @{system_option show_main_goal}
"show-main-goal"
"Show main goal in proof state display";
val _ =
ProofGeneral.preference_option ProofGeneral.category_display
NONE
- @{option eta_contract}
+ @{system_option eta_contract}
"eta-contract"
"Print terms eta-contracted";
@@ -69,7 +69,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_advanced_display
NONE
- @{option goals_limit}
+ @{system_option goals_limit}
"goals-limit"
"Setting for maximum number of subgoals to be printed";
@@ -85,7 +85,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_advanced_display
NONE
- @{option show_question_marks}
+ @{system_option show_question_marks}
"show-question-marks"
"Show leading question mark of variable name";
@@ -123,7 +123,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option ML_exception_trace}
+ @{system_option ML_exception_trace}
"debugging"
"Whether to enable exception trace for toplevel command execution";
@@ -140,14 +140,14 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_proof
(SOME "true")
- @{option quick_and_dirty}
+ @{system_option quick_and_dirty}
"quick-and-dirty"
"Take a few short cuts";
val _ =
ProofGeneral.preference_option ProofGeneral.category_proof
NONE
- @{option skip_proofs}
+ @{system_option skip_proofs}
"skip-proofs"
"Skip over proofs";
--- a/src/Tools/jEdit/src/document_model.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Tue Apr 08 23:16:00 2014 +0200
@@ -119,7 +119,7 @@
for {
cmd <- snapshot.node.load_commands
blob_name <- cmd.blobs_names
- blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
+ blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
start <- snapshot.node.command_start(cmd)
range = snapshot.convert(cmd.proper_range + start)
@@ -138,7 +138,7 @@
/* blob */
- private var _blob: Option[(Bytes, Command.File)] = None // owned by Swing thread
+ private var _blob: Option[(Bytes, Text.Chunk)] = None // owned by Swing thread
private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
@@ -146,17 +146,17 @@
Swing_Thread.require {
if (is_theory) None
else {
- val (bytes, file) =
+ val (bytes, chunk) =
_blob match {
case Some(x) => x
case None =>
val bytes = PIDE.resources.file_content(buffer)
- val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
- _blob = Some((bytes, file))
- (bytes, file)
+ val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
+ _blob = Some((bytes, chunk))
+ (bytes, chunk)
}
val changed = pending_edits.is_pending()
- Some(Document.Blob(bytes, file, changed))
+ Some(Document.Blob(bytes, chunk, changed))
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 08 23:16:00 2014 +0200
@@ -52,7 +52,7 @@
{
Swing_Thread.require()
- JEdit_Lib.jedit_buffer(name.node) match {
+ JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
PIDE.document_model(buffer) match {
case Some(model) => model.snapshot
@@ -159,6 +159,55 @@
/* hyperlinks */
+ def hyperlink_url(name: String): Hyperlink =
+ new Hyperlink {
+ def follow(view: View) =
+ default_thread_pool.submit(() =>
+ try { Isabelle_System.open(name) }
+ catch {
+ case exn: Throwable =>
+ GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+ })
+ override def toString: String = "URL " + quote(name)
+ }
+
+ def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
+ new Hyperlink {
+ def follow(view: View) = goto_file(view, name, line, column)
+ override def toString: String = "file " + quote(name)
+ }
+
+ def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
+ : Option[Hyperlink] =
+ {
+ val opt_name =
+ if (Path.is_wellformed(source_name)) {
+ if (Path.is_valid(source_name)) {
+ val path = Path.explode(source_name)
+ Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
+ }
+ else None
+ }
+ else Some(source_name)
+
+ opt_name match {
+ case Some(name) =>
+ JEdit_Lib.jedit_buffer(name) match {
+ case Some(buffer) if offset > 0 =>
+ val (line, column) =
+ JEdit_Lib.buffer_lock(buffer) {
+ ((1, 1) /:
+ (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+ zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
+ Symbol.advance_line_column)
+ }
+ Some(hyperlink_file(name, line, column))
+ case _ => Some(hyperlink_file(name, line))
+ }
+ case None => None
+ }
+ }
+
override def hyperlink_command(
snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
{
@@ -171,9 +220,9 @@
val sources_iterator =
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
(if (offset == 0) Iterator.empty
- else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+ else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
- Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
+ Some(hyperlink_file(file_name, line, column))
}
}
}
@@ -188,43 +237,4 @@
case None => None
}
}
-
- def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
- new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
-
- def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
- : Option[Hyperlink] =
- {
- if (Path.is_valid(source_name)) {
- Isabelle_System.source_file(Path.explode(source_name)) match {
- case Some(path) =>
- val name = Isabelle_System.platform_path(path)
- JEdit_Lib.jedit_buffer(name) match {
- case Some(buffer) if offset > 0 =>
- val (line, column) =
- JEdit_Lib.buffer_lock(buffer) {
- ((1, 1) /:
- (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
- zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
- Symbol.advance_line_column)
- }
- Some(hyperlink_file(name, line, column))
- case _ => Some(hyperlink_file(name, line))
- }
- case None => None
- }
- }
- else None
- }
-
- def hyperlink_url(name: String): Hyperlink =
- new Hyperlink {
- def follow(view: View) =
- default_thread_pool.submit(() =>
- try { Isabelle_System.open(name) }
- catch {
- case exn: Throwable =>
- GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
- })
- }
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Apr 08 23:16:00 2014 +0200
@@ -120,6 +120,9 @@
def jedit_buffer(name: String): Option[Buffer] =
jedit_buffers().find(buffer => buffer_name(buffer) == name)
+ def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
+ jedit_buffer(name.node)
+
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
--- a/src/Tools/jEdit/src/jedit_resources.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Tue Apr 08 23:16:00 2014 +0200
@@ -57,7 +57,7 @@
override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
{
Swing_Thread.now {
- JEdit_Lib.jedit_buffer(name.node) match {
+ JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
JEdit_Lib.buffer_lock(buffer) {
Some(f(buffer.getSegment(0, buffer.getLength)))
@@ -120,7 +120,6 @@
override def commit(change: Session.Change)
{
if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
- if (change.deps_changed) PIDE.deps_changed()
}
}
--- a/src/Tools/jEdit/src/rendering.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Tue Apr 08 23:16:00 2014 +0200
@@ -321,15 +321,18 @@
/* hyperlinks */
+ private def jedit_file(name: String): String =
+ if (Path.is_valid(name))
+ PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
+ else name
+
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
range, Vector.empty, Rendering.hyperlink_elements, _ =>
{
- case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
- if Path.is_valid(name) =>
- val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
- val link = PIDE.editor.hyperlink_file(jedit_file)
+ case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
+ val link = PIDE.editor.hyperlink_file(jedit_file(name))
Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
@@ -457,10 +460,11 @@
"\n" + t.message
else ""
Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
- case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
- if Path.is_valid(name) =>
- val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
- val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
+ case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
+ val file = jedit_file(name)
+ val text =
+ if (name == file) "file " + quote(file)
+ else "path " + quote(name) + "\nfile " + quote(file)
Some(add(prev, r, (true, XML.Text(text))))
case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Apr 08 23:16:00 2014 +0200
@@ -41,7 +41,7 @@
if (in_checkbox(peer.indexToLocation(index), point)) {
if (clicks == 1) {
for {
- buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
+ buffer <- JEdit_Lib.jedit_buffer(listData(index))
model <- PIDE.document_model(buffer)
} model.node_required = !model.node_required
}
--- a/src/Tools/quickcheck.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/quickcheck.ML Tue Apr 08 23:16:00 2014 +0200
@@ -95,7 +95,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_quickcheck}
+ @{system_option auto_quickcheck}
"auto-quickcheck"
"Run Quickcheck automatically";
@@ -584,7 +584,7 @@
end
|> `(fn (outcome_code, _) => outcome_code = genuineN);
-val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
+val _ = Try.tool_setup (quickcheckN, (20, @{system_option auto_quickcheck}, try_quickcheck));
end;
--- a/src/Tools/solve_direct.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/solve_direct.ML Tue Apr 08 23:16:00 2014 +0200
@@ -37,7 +37,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option auto_solve_direct}
+ @{system_option auto_solve_direct}
"auto-solve-direct"
("Run " ^ quote solve_directN ^ " automatically");
@@ -115,6 +115,6 @@
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
-val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
+val _ = Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct));
end;
--- a/src/Tools/try.ML Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/try.ML Tue Apr 08 23:16:00 2014 +0200
@@ -32,7 +32,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
(SOME "4.0")
- @{option auto_time_limit}
+ @{system_option auto_time_limit}
"auto-try-time-limit"
"Time limit for automatically tried tools (in seconds)"
@@ -103,7 +103,7 @@
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
let
- val auto_time_limit = Options.default_real @{option auto_time_limit}
+ val auto_time_limit = Options.default_real @{system_option auto_time_limit}
in
if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
@@ -120,7 +120,7 @@
(fn {command_name, ...} =>
if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
SOME
- {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
+ {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
pri = ~ weight,
persistent = true,
strict = true,
@@ -128,7 +128,7 @@
let
val state = Toplevel.proof_of st
|> Proof.map_context (Context_Position.set_visible false)
- val auto_time_limit = Options.default_real @{option auto_time_limit}
+ val auto_time_limit = Options.default_real @{system_option auto_time_limit}
in
if auto_time_limit > 0.0 then
(case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of