# HG changeset patch # User wenzelm # Date 1396991760 -7200 # Node ID 92345da2349f86ae449c013c5f08da2333f5bce1 # Parent 39281b3e4facfce8fd0ed04ed2a524b1960ea18a# Parent 57b5c8db55f1d38b2c2c736299d214d829a06031 merged diff -r 39281b3e4fac -r 92345da2349f src/Doc/JEdit/JEdit.thy --- 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 diff -r 39281b3e4fac -r 92345da2349f src/Doc/antiquote_setup.ML --- 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} #> diff -r 39281b3e4fac -r 92345da2349f src/HOL/Mutabelle/mutabelle_extra.ML --- 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) diff -r 39281b3e4fac -r 92345da2349f src/HOL/Prolog/prolog.ML --- 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 diff -r 39281b3e4fac -r 92345da2349f src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML --- 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" diff -r 39281b3e4fac -r 92345da2349f src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- 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) *} diff -r 39281b3e4fac -r 92345da2349f src/HOL/Tools/Nitpick/nitpick_commands.ML --- 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; diff -r 39281b3e4fac -r 92345da2349f src/HOL/Tools/SMT/smt_setup_solvers.ML --- 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 diff -r 39281b3e4fac -r 92345da2349f src/HOL/Tools/SMT2/smt2_systems.ML --- 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 diff -r 39281b3e4fac -r 92345da2349f src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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} => diff -r 39281b3e4fac -r 92345da2349f src/HOL/Tools/try0.ML --- 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; diff -r 39281b3e4fac -r 92345da2349f src/Pure/General/position.ML --- 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]; diff -r 39281b3e4fac -r 92345da2349f src/Pure/General/position.scala --- 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 } } diff -r 39281b3e4fac -r 92345da2349f src/Pure/General/symbol.scala --- 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 { diff -r 39281b3e4fac -r 92345da2349f src/Pure/Isar/isar_syn.ML --- 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)))); diff -r 39281b3e4fac -r 92345da2349f src/Pure/Isar/parse.scala --- 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) diff -r 39281b3e4fac -r 92345da2349f src/Pure/Isar/token.scala --- 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)) } diff -r 39281b3e4fac -r 92345da2349f src/Pure/ML/ml_antiquotations.ML --- 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)) => diff -r 39281b3e4fac -r 92345da2349f src/Pure/ML/ml_lex.ML --- 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; diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/command.ML --- 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) diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/command.scala --- 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 */ diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/document.ML --- 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); diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/document.scala --- 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) diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/markup.ML --- 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"; diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/protocol.ML --- 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 diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/protocol.scala --- 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)) } diff -r 39281b3e4fac -r 92345da2349f src/Pure/PIDE/text.scala --- 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 diff -r 39281b3e4fac -r 92345da2349f src/Pure/System/isabelle_system.scala --- 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) = diff -r 39281b3e4fac -r 92345da2349f src/Pure/System/options.ML --- 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; diff -r 39281b3e4fac -r 92345da2349f src/Pure/System/options.scala --- 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) } diff -r 39281b3e4fac -r 92345da2349f src/Pure/Thy/thy_syntax.scala --- 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) }) } diff -r 39281b3e4fac -r 92345da2349f src/Pure/Tools/build.scala --- 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)] diff -r 39281b3e4fac -r 92345da2349f src/Pure/Tools/find_theorems.ML --- 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 = diff -r 39281b3e4fac -r 92345da2349f src/Pure/Tools/proof_general_pure.ML --- 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"; diff -r 39281b3e4fac -r 92345da2349f src/Tools/jEdit/src/document_model.scala --- 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)) } } diff -r 39281b3e4fac -r 92345da2349f src/Tools/jEdit/src/jedit_editor.scala --- 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))) - }) - } } diff -r 39281b3e4fac -r 92345da2349f src/Tools/jEdit/src/jedit_lib.scala --- 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] = diff -r 39281b3e4fac -r 92345da2349f src/Tools/jEdit/src/jedit_resources.scala --- 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() } } diff -r 39281b3e4fac -r 92345da2349f src/Tools/jEdit/src/rendering.scala --- 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))))) diff -r 39281b3e4fac -r 92345da2349f src/Tools/jEdit/src/theories_dockable.scala --- 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 } diff -r 39281b3e4fac -r 92345da2349f src/Tools/quickcheck.ML --- 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; diff -r 39281b3e4fac -r 92345da2349f src/Tools/solve_direct.ML --- 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; diff -r 39281b3e4fac -r 92345da2349f src/Tools/try.ML --- 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