--- a/src/Pure/General/bytes.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/General/bytes.scala Wed Nov 20 16:43:09 2013 +0100
@@ -89,7 +89,7 @@
/* content */
- def sha1_digest: SHA1.Digest = SHA1.digest(bytes)
+ lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
override def toString: String =
UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
--- a/src/Pure/Isar/keyword.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Isar/keyword.ML Wed Nov 20 16:43:09 2013 +0100
@@ -51,7 +51,7 @@
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
val is_keyword: string -> bool
val command_keyword: string -> T option
- val command_files: string -> string list
+ val command_files: string -> Path.T -> Path.T list
val command_tags: string -> string list
val dest: unit -> string list * string list
val define: string * T option -> unit
@@ -196,7 +196,15 @@
in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
fun command_keyword name = Symtab.lookup (get_commands ()) name;
-val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
+
+fun command_files name path =
+ (case command_keyword name of
+ NONE => []
+ | SOME (Keyword {kind, files, ...}) =>
+ if kind <> kind_of thy_load then []
+ else if null files then [path]
+ else map (fn ext => Path.ext ext path) files);
+
val command_tags = these o Option.map tags_of o command_keyword;
fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
--- a/src/Pure/Isar/outer_syntax.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Wed Nov 20 16:43:09 2013 +0100
@@ -58,11 +58,11 @@
def thy_load(span: List[Token]): Option[List[String]] =
keywords.get(Command.name(span)) match {
- case Some((Keyword.THY_LOAD, files)) => Some(files)
+ case Some((Keyword.THY_LOAD, exts)) => Some(exts)
case _ => None
}
- def thy_load_commands: List[(String, List[String])] =
+ val thy_load_commands: List[(String, List[String])] =
(for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
--- a/src/Pure/Isar/token.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Isar/token.ML Wed Nov 20 16:43:09 2013 +0100
@@ -13,7 +13,7 @@
type file = {src_path: Path.T, text: string, pos: Position.T}
datatype value =
Text of string | Typ of typ | Term of term | Fact of thm list |
- Attribute of morphism -> attribute | Files of file list
+ Attribute of morphism -> attribute | Files of file Exn.result list
type T
val str_of_kind: kind -> string
val position_of: T -> Position.T
@@ -46,8 +46,8 @@
val content_of: T -> string
val unparse: T -> string
val text_of: T -> string * string
- val get_files: T -> file list option
- val put_files: file list -> T -> T
+ val get_files: T -> file Exn.result list
+ val put_files: file Exn.result list -> T -> T
val get_value: T -> value option
val map_value: (value -> value) -> T -> T
val mk_text: string -> T
@@ -88,7 +88,7 @@
Term of term |
Fact of thm list |
Attribute of morphism -> attribute |
- Files of file list;
+ Files of file Exn.result list;
datatype slot =
Slot |
@@ -244,10 +244,11 @@
(* inlined file content *)
-fun get_files (Token (_, _, Value (SOME (Files files)))) = SOME files
- | get_files _ = NONE;
+fun get_files (Token (_, _, Value (SOME (Files files)))) = files
+ | get_files _ = [];
-fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
+fun put_files [] tok = tok
+ | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
| put_files _ tok =
raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
--- a/src/Pure/PIDE/command.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/command.ML Wed Nov 20 16:43:09 2013 +0100
@@ -6,13 +6,15 @@
signature COMMAND =
sig
- val read: (unit -> theory) -> Token.T list -> Toplevel.transition
+ type blob = (string * string 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
val eval_eq: eval * eval -> bool
val eval_running: eval -> bool
val eval_finished: eval -> bool
val eval_result_state: eval -> Toplevel.state
- val eval: (unit -> theory) -> Token.T list -> eval -> eval
+ val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
type print
val print: bool -> (string * string list) list -> string ->
eval -> print list -> print list option
@@ -82,7 +84,38 @@
(* read *)
-fun read init span =
+type blob = (string * string option) Exn.result; (*file node name, digest or text*)
+
+fun read_file master_dir pos src_path =
+ let
+ val full_path = File.check_file (File.full_path master_dir src_path);
+ val _ = Position.report pos (Markup.path (Path.implode full_path));
+ in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
+
+fun resolve_files master_dir blobs toks =
+ (case Thy_Syntax.parse_spans toks of
+ [span] => span
+ |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
+ let
+ 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, SOME text)) =
+ let val _ = Position.report pos (Markup.path file)
+ in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
+ | 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)
+ else if length src_paths = length blobs then
+ map2 make_file src_paths blobs
+ else error ("Misalignment of inlined files" ^ Position.here pos)
+ end)
+ |> Thy_Syntax.span_content
+ | _ => toks);
+
+fun read init master_dir blobs span =
let
val outer_syntax = #2 (Outer_Syntax.get_syntax ());
val command_reports = Outer_Syntax.command_reports outer_syntax;
@@ -99,7 +132,7 @@
in
if is_malformed then Toplevel.malformed pos "Malformed command syntax"
else
- (case Outer_Syntax.read_spans outer_syntax span of
+ (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
[tr] =>
if Keyword.is_control (Toplevel.name_of tr) then
Toplevel.malformed pos "Illegal control command"
@@ -180,14 +213,14 @@
in
-fun eval init span eval0 =
+fun eval init master_dir blobs span eval0 =
let
val exec_id = Document_ID.make ();
fun process () =
let
val tr =
Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
- (fn () => read init span |> Toplevel.exec_id exec_id) ();
+ (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
in eval_state span tr (eval_result eval0) end;
in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
--- a/src/Pure/PIDE/command.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/command.scala Wed Nov 20 16:43:09 2013 +0100
@@ -144,11 +144,13 @@
def name(span: List[Token]): String =
span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
+ type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])]
+
def apply(
id: Document_ID.Command,
node_name: Document.Node.Name,
+ blobs: List[Blob],
span: List[Token],
- thy_load: Option[List[String]],
results: Results = Results.empty,
markup: Markup_Tree = Markup_Tree.empty): Command =
{
@@ -167,14 +169,14 @@
i += n
}
- new Command(id, node_name, span1.toList, source, thy_load, results, markup)
+ new Command(id, node_name, blobs, span1.toList, source, results, markup)
}
- val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, None)
+ val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
: Command =
- Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), None,
+ Command(id, Document.Node.Name.empty, Nil, List(Token(Token.Kind.UNPARSED, source)),
results, markup)
def unparsed(source: String): Command =
@@ -213,9 +215,9 @@
final class Command private(
val id: Document_ID.Command,
val node_name: Document.Node.Name,
+ val blobs: List[Command.Blob],
val span: List[Token],
val source: String,
- val thy_load: Option[List[String]],
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
@@ -235,6 +237,15 @@
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
+ /* blobs */
+
+ def blobs_names: List[Document.Node.Name] =
+ for (Exn.Res((name, _)) <- blobs) yield name
+
+ def blobs_digests: List[SHA1.Digest] =
+ for (Exn.Res((_, Some(digest))) <- blobs) yield digest
+
+
/* source */
def length: Int = source.length
--- a/src/Pure/PIDE/document.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/document.ML Wed Nov 20 16:43:09 2013 +0100
@@ -18,7 +18,9 @@
type edit = string * node_edit
type state
val init_state: state
- val define_command: Document_ID.command -> string -> string -> state -> state
+ val define_blob: string -> string -> state -> state
+ val define_command: Document_ID.command -> string -> Command.blob list -> string ->
+ state -> state
val remove_versions: Document_ID.version list -> state -> state
val start_execution: state -> state
val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -70,7 +72,7 @@
visible_last = try List.last command_ids,
overlays = Inttab.make_list overlays};
-val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
val no_perspective = make_perspective (false, [], []);
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
@@ -88,9 +90,14 @@
fun read_header node span =
let
- val (dir, {name = (name, _), imports, keywords}) = get_header node;
+ val {name = (name, _), imports, keywords} = #2 (get_header node);
val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
- in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
+ in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
+
+fun master_directory node =
+ (case try Url.explode (#1 (get_header node)) of
+ SOME (Url.File path) => path
+ | _ => Path.current);
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective args =
@@ -231,29 +238,32 @@
abstype state = State of
{versions: version Inttab.table, (*version id -> document content*)
- commands: (string * Token.T list lazy) Inttab.table, (*command id -> named command span*)
+ blobs: string Symtab.table, (*digest -> text*)
+ commands: (string * Command.blob list * Token.T list lazy) Inttab.table,
+ (*command id -> name, inlined files, command span*)
execution: execution} (*current execution process*)
with
-fun make_state (versions, commands, execution) =
- State {versions = versions, commands = commands, execution = execution};
+fun make_state (versions, blobs, commands, execution) =
+ State {versions = versions, blobs = blobs, commands = commands, execution = execution};
-fun map_state f (State {versions, commands, execution}) =
- make_state (f (versions, commands, execution));
+fun map_state f (State {versions, blobs, commands, execution}) =
+ make_state (f (versions, blobs, commands, execution));
val init_state =
- make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
+ make_state (Inttab.make [(Document_ID.none, empty_version)],
+ Symtab.empty, Inttab.empty, no_execution);
(* document versions *)
fun define_version version_id version =
- map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
+ map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
let
val versions' = Inttab.update_new (version_id, version) versions
handle Inttab.DUP dup => err_dup "document version" dup;
val execution' = new_execution version_id delay_request frontier;
- in (versions', commands, execution') end);
+ in (versions', blobs, commands, execution') end);
fun the_version (State {versions, ...}) version_id =
(case Inttab.lookup versions version_id of
@@ -265,10 +275,23 @@
handle Inttab.UNDEF _ => err_undef "document version" version_id;
+(* inlined files *)
+
+fun define_blob digest text =
+ map_state (fn (versions, blobs, commands, execution) =>
+ let val blobs' = Symtab.update (digest, text) blobs
+ in (versions, blobs', commands, execution) end);
+
+fun the_blob (State {blobs, ...}) digest =
+ (case Symtab.lookup blobs digest of
+ NONE => error ("Undefined blob: " ^ digest)
+ | SOME text => text);
+
+
(* commands *)
-fun define_command command_id name text =
- map_state (fn (versions, commands, execution) =>
+fun define_command command_id name command_blobs text =
+ map_state (fn (versions, blobs, commands, execution) =>
let
val id = Document_ID.print command_id;
val span =
@@ -279,9 +302,9 @@
Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
val commands' =
- Inttab.update_new (command_id, (name, span)) commands
+ Inttab.update_new (command_id, (name, command_blobs, span)) commands
handle Inttab.DUP dup => err_dup "command" dup;
- in (versions, commands', execution) end);
+ in (versions, blobs, commands', execution) end);
fun the_command (State {commands, ...}) command_id =
(case Inttab.lookup commands command_id of
@@ -295,7 +318,7 @@
(* remove_versions *)
-fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
+fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) =>
let
val _ =
member (op =) version_ids (#version_id execution) andalso
@@ -308,12 +331,17 @@
String_Graph.fold (fn (_, (node, _)) => node |>
iterate_entries (fn ((_, command_id), _) =>
SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
- in (versions', commands', execution) end);
+ val blobs' =
+ (commands', Symtab.empty) |->
+ Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
+ fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
+
+ in (versions', blobs', commands', execution) end);
(* document execution *)
-fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
+fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
timeit "Document.start_execution" (fn () =>
let
val {version_id, execution_id, delay_request, frontier} = execution;
@@ -350,7 +378,7 @@
val execution' =
{version_id = version_id, execution_id = execution_id,
delay_request = delay_request', frontier = frontier'};
- in (versions, commands, execution') end));
+ in (versions, blobs, commands, execution') end));
@@ -391,18 +419,19 @@
Symtab.update (a, ())) all_visible all_required
end;
+fun loaded_theory name =
+ (case try (unsuffix ".thy") name of
+ SOME a => Thy_Info.lookup_theory a
+ | NONE => NONE);
+
fun init_theory deps node span =
let
- (* FIXME provide files via Isabelle/Scala, not master_dir *)
- val (dir, header) = read_header node span;
- val master_dir =
- (case try Url.explode dir of
- SOME (Url.File path) => path
- | _ => Path.current);
+ val master_dir = master_directory node;
+ val header = read_header node span;
val imports = #imports header;
val parents =
imports |> map (fn (import, _) =>
- (case Thy_Info.lookup_theory import of
+ (case loaded_theory import of
SOME thy => thy
| NONE =>
Toplevel.end_theory (Position.file_only import)
@@ -413,7 +442,7 @@
in Thy_Load.begin_theory master_dir header parents end;
fun check_theory full name node =
- is_some (Thy_Info.lookup_theory name) orelse
+ is_some (loaded_theory name) orelse
can get_header node andalso (not full orelse is_some (get_result node));
fun last_common state node_required node0 node =
@@ -471,9 +500,13 @@
val command_visible = visible_command node command_id';
val command_overlays = overlays node command_id';
- val (command_name, span) = the_command state command_id' ||> Lazy.force;
+ val (command_name, blobs0, span0) = the_command state command_id';
+ val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blobs0;
+ val span = Lazy.force span0;
- val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
+ val eval' =
+ Command.eval (fn () => the_default illegal_init init span)
+ (master_directory node) blobs span eval;
val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
val exec' = (eval', prints');
--- a/src/Pure/PIDE/document.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/document.scala Wed Nov 20 16:43:09 2013 +0100
@@ -47,6 +47,8 @@
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[Command.Edit, Command.Perspective]
+ type Blobs = Map[Node.Name, Bytes]
+
object Node
{
val empty: Node = new Node()
@@ -64,9 +66,11 @@
def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
+ val no_header = bad_header("No theory header")
+
object Name
{
- val empty = Name("", "", "")
+ val empty = Name("")
object Ordering extends scala.math.Ordering[Name]
{
@@ -74,7 +78,7 @@
}
}
- sealed case class Name(node: String, dir: String, theory: String)
+ sealed case class Name(node: String, master_dir: String = "", theory: String = "")
{
override def hashCode: Int = node.hashCode
override def equals(that: Any): Boolean =
@@ -82,7 +86,9 @@
case other: Name => node == other.node
case _ => false
}
- override def toString: String = theory
+
+ def is_theory: Boolean = !theory.isEmpty
+ override def toString: String = if (is_theory) theory else node
}
@@ -121,6 +127,7 @@
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
case class Deps[A, B](header: Header) extends Edit[A, B]
case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
+ case class Blob[A, B]() extends Edit[A, B]
type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
@@ -149,7 +156,7 @@
final class Commands private(val commands: Linear_Set[Command])
{
lazy val thy_load_commands: List[Command] =
- commands.iterator.filter(_.thy_load.isDefined).toList
+ commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
{
@@ -246,6 +253,14 @@
def entries: Iterator[(Node.Name, Node)] =
graph.entries.map({ case (name, (node, _)) => (name, node) })
+ def thy_load_commands(file_name: Node.Name): List[Command] =
+ (for {
+ (_, node) <- entries
+ cmd <- node.thy_load_commands.iterator
+ name <- cmd.blobs_names.iterator
+ if name == file_name
+ } yield cmd).toList
+
def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
def topological_order: List[Node.Name] = graph.topological_order
}
@@ -392,6 +407,7 @@
final case class State private(
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
val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
@@ -406,6 +422,9 @@
assignments = assignments + (id -> assignment.unfinished))
}
+ def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest)
+ def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
+
def define_command(command: Command): State =
{
val id = command.id
@@ -509,6 +528,7 @@
{
val versions1 = versions -- removed
val assignments1 = assignments -- removed
+ var blobs1 = Set.empty[SHA1.Digest]
var commands1 = Map.empty[Document_ID.Command, Command.State]
var execs1 = Map.empty[Document_ID.Exec, Command.State]
for {
@@ -517,14 +537,19 @@
(_, node) <- version.nodes.entries
command <- node.commands.iterator
} {
+ for (digest <- command.blobs_digests; if !blobs1.contains(digest))
+ blobs1 += digest
+
if (!commands1.isDefinedAt(command.id))
commands.get(command.id).foreach(st => commands1 += (command.id -> st))
+
for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
if (!execs1.isDefinedAt(exec_id))
execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
}
}
- copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
+ copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
+ assignments = assignments1)
}
def command_state(version: Version, command: Command): Command.State =
--- a/src/Pure/PIDE/protocol.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML Wed Nov 20 16:43:09 2013 +0100
@@ -23,9 +23,23 @@
end);
val _ =
+ Isabelle_Process.protocol_command "Document.define_blob"
+ (fn [digest, content] => Document.change_state (Document.define_blob digest content));
+
+val _ =
Isabelle_Process.protocol_command "Document.define_command"
- (fn [id, name, text] =>
- Document.change_state (Document.define_command (Document_ID.parse id) name text));
+ (fn [id, name, blobs_yxml, text] =>
+ let
+ val blobs =
+ YXML.parse_body blobs_yxml |>
+ let open XML.Decode in
+ list (variant
+ [fn ([], a) => Exn.Res (pair string (option string) a),
+ fn ([], a) => Exn.Exn (ERROR (string a))])
+ end;
+ in
+ Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
+ end);
val _ =
Isabelle_Process.protocol_command "Document.discontinue_execution"
--- a/src/Pure/PIDE/protocol.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Nov 20 16:43:09 2013 +0100
@@ -308,11 +308,28 @@
trait Protocol extends Isabelle_Process
{
+ /* inlined files */
+
+ def define_blob(blob: Bytes): Unit =
+ protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob)
+
+
/* commands */
def define_command(command: Command): Unit =
+ {
+ val blobs_yxml =
+ { import XML.Encode._
+ val encode_blob: T[Command.Blob] =
+ variant(List(
+ { case Exn.Res((a, b)) =>
+ (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
+ { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+ YXML.string_of_body(list(encode_blob)(command.blobs))
+ }
protocol_command("Document.define_command",
- Document_ID(command.id), encode(command.name), encode(command.source))
+ Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
+ }
/* execution */
@@ -335,10 +352,11 @@
def encode_edit(name: Document.Node.Name)
: T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
variant(List(
+ // FIXME Document.Node.Blob (!??)
{ case Document.Node.Clear() => (Nil, Nil) }, // FIXME unused !?
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Deps(header) =>
- val dir = Isabelle_System.posix_path(name.dir)
+ val master_dir = Isabelle_System.posix_path(name.master_dir)
val imports = header.imports.map(_.node)
val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
(Nil,
@@ -346,7 +364,7 @@
pair(list(pair(Encode.string,
option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
list(Encode.string)))))(
- (dir, (name.theory, (imports, (keywords, header.errors)))))) },
+ (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
{ case Document.Node.Perspective(a, b, c) =>
(bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
--- a/src/Pure/System/session.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/System/session.scala Wed Nov 20 16:43:09 2013 +0100
@@ -25,7 +25,7 @@
case class Statistics(props: Properties.T)
case class Global_Options(options: Options)
case object Caret_Focus
- case class Raw_Edits(edits: List[Document.Edit_Text])
+ case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
case class Commands_Changed(
assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -167,6 +167,7 @@
//{{{
private case class Text_Edits(
previous: Future[Document.Version],
+ doc_blobs: Document.Blobs,
text_edits: List[Document.Edit_Text],
version_result: Promise[Document.Version])
@@ -177,14 +178,14 @@
receive {
case Stop => finished = true; reply(())
- case Text_Edits(previous, text_edits, version_result) =>
+ case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
val prev = previous.get_finished
val (doc_edits, version) =
Timing.timeit("Thy_Load.text_edits", timing) {
- thy_load.text_edits(reparse_limit, prev, text_edits)
+ thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
}
version_result.fulfill(version)
- sender ! Change(doc_edits, prev, version)
+ sender ! Change(doc_blobs, doc_edits, prev, version)
case bad => System.err.println("change_parser: ignoring bad message " + bad)
}
@@ -250,6 +251,7 @@
private case class Start(args: List[String])
private case class Cancel_Exec(exec_id: Document_ID.Exec)
private case class Change(
+ doc_blobs: Document.Blobs,
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
version: Document.Version)
@@ -348,7 +350,7 @@
/* raw edits */
- def handle_raw_edits(edits: List[Document.Edit_Text])
+ def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
//{{{
{
prover.get.discontinue_execution()
@@ -357,8 +359,8 @@
val version = Future.promise[Document.Version]
val change = global_state >>> (_.continue_history(previous, edits, version))
- raw_edits.event(Session.Raw_Edits(edits))
- change_parser ! Text_Edits(previous, edits, version)
+ raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
+ change_parser ! Text_Edits(previous, doc_blobs, edits, version)
}
//}}}
@@ -374,6 +376,18 @@
def id_command(command: Command)
{
+ for {
+ digest <- command.blobs_digests
+ if !global_state().defined_blob(digest)
+ } {
+ change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+ case Some(blob) =>
+ global_state >> (_.define_blob(digest))
+ prover.get.define_blob(blob)
+ case None => System.err.println("Missing blob for SHA1 digest " + digest)
+ }
+ }
+
if (!global_state().defined_command(command.id)) {
global_state >> (_.define_command(command))
prover.get.define_command(command)
@@ -510,7 +524,7 @@
case Update_Options(options) if prover.isDefined =>
if (is_ready) {
prover.get.options(options)
- handle_raw_edits(Nil)
+ handle_raw_edits(Map.empty, Nil)
}
global_options.event(Session.Global_Options(options))
reply(())
@@ -518,8 +532,8 @@
case Cancel_Exec(exec_id) if prover.isDefined =>
prover.get.cancel_exec(exec_id)
- case Session.Raw_Edits(edits) if prover.isDefined =>
- handle_raw_edits(edits)
+ case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
+ handle_raw_edits(doc_blobs, edits)
reply(())
case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
@@ -572,8 +586,8 @@
def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
- def update(edits: List[Document.Edit_Text])
- { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
+ def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+ { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
def update_options(options: Options)
{ session_actor !? Update_Options(options) }
--- a/src/Pure/Thy/thy_info.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala Wed Nov 20 16:43:09 2013 +0100
@@ -68,7 +68,7 @@
val dep_files =
rev_deps.par.map(dep =>
Exn.capture {
- dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a))
+ dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
}).toList
((Nil: List[Path]) /: dep_files) {
case (acc_files, files) => Exn.release(files) ::: acc_files
--- a/src/Pure/Thy/thy_load.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML Wed Nov 20 16:43:09 2013 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/Thy/thy_load.ML
Author: Makarius
-Loading files that contribute to a theory.
+Management of theory sources and auxiliary files.
*)
signature THY_LOAD =
@@ -9,11 +9,10 @@
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val thy_path: Path.T -> Path.T
- val read_files: Path.T -> string -> Path.T * Position.T -> Token.file list
- val parse_files: string -> (theory -> Token.file list) parser
val check_thy: Path.T -> string ->
{master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
imports: (string * Position.T) list, keywords: Thy_Header.keywords}
+ val parse_files: string -> (theory -> Token.file list) parser
val provide: Path.T * SHA1.digest -> theory -> theory
val provide_parse_files: string -> (theory -> Token.file list * theory) parser
val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
@@ -56,34 +55,12 @@
fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
-(* auxiliary files *)
-
-fun check_file dir file = File.check_file (File.full_path dir file);
-
-fun read_files dir cmd (path, pos) =
- let
- fun make_file file =
- let
- val _ = Position.report pos (Markup.path (Path.implode file));
- val full_path = check_file dir file;
- in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
- val paths =
- (case Keyword.command_files cmd of
- [] => [path]
- | exts => map (fn ext => Path.ext ext path) exts);
- in map make_file paths end;
-
-fun parse_files cmd =
- Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
- (case Token.get_files tok of
- SOME files => files
- | NONE => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)));
-
-
(* theory files *)
val thy_path = Path.ext "thy";
+fun check_file dir file = File.check_file (File.full_path dir file);
+
fun check_thy dir thy_name =
let
val path = thy_path (Path.basic thy_name);
@@ -102,6 +79,17 @@
(* load files *)
+fun parse_files cmd =
+ Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
+ (case Token.get_files tok of
+ [] =>
+ let
+ val master_dir = master_directory thy;
+ val pos = Token.position_of tok;
+ val src_paths = Keyword.command_files cmd (Path.explode name);
+ in map (Command.read_file master_dir pos) src_paths end
+ | files => map Exn.release files));
+
fun provide (src_path, id) =
map_files (fn (master_dir, imports, provided) =>
if AList.defined (op =) provided src_path then
@@ -135,18 +123,18 @@
in map (File.full_path master_dir o #1) provided end;
-(* load_thy *)
+(* load theory *)
fun begin_theory master_dir {name, imports, keywords} parents =
Theory.begin_theory name parents
|> put_deps master_dir imports
|> fold Thy_Header.declare_keyword keywords;
-fun excursion last_timing init elements =
+fun excursion master_dir last_timing init elements =
let
fun prepare_span span =
Thy_Syntax.span_content span
- |> Command.read init
+ |> Command.read init master_dir []
|> (fn tr => Toplevel.put_timing (last_timing tr) tr);
fun element_result span_elem (st, _) =
@@ -171,7 +159,7 @@
val lexs = Keyword.get_lexicons ();
val toks = Thy_Syntax.parse_tokens lexs text_pos text;
- val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
+ val spans = Thy_Syntax.parse_spans toks;
val elements = Thy_Syntax.parse_elements spans;
fun init () =
@@ -180,7 +168,8 @@
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
+ val (results, thy) =
+ cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
fun present () =
--- a/src/Pure/Thy/thy_load.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_load.scala Wed Nov 20 16:43:09 2013 +0100
@@ -21,23 +21,23 @@
def is_ok(str: String): Boolean =
try { thy_path(Path.explode(str)); true }
catch { case ERROR(_) => false }
-
-
- /* document node names */
-
- def path_node_name(raw_path: Path): Document.Node.Name =
- {
- val path = raw_path.expand
- val node = path.implode
- val dir = path.dir.implode
- val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
- Document.Node.Name(node, dir, theory)
- }
}
class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
{
+ /* document node names */
+
+ def node_name(raw_path: Path): Document.Node.Name =
+ {
+ val path = raw_path.expand
+ val node = path.implode
+ val theory = Thy_Header.thy_name(node).getOrElse("")
+ val master_dir = if (theory == "") "" else path.dir.implode
+ Document.Node.Name(node, master_dir, theory)
+ }
+
+
/* file-system operations */
def append(dir: String, source_path: Path): String =
@@ -56,50 +56,24 @@
/* theory files */
- private def find_file(tokens: List[Token]): Option[String] =
- {
- def clean(toks: List[Token]): List[Token] =
- toks match {
- case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
- case t :: ts => t :: clean(ts)
- case Nil => Nil
- }
- val clean_tokens = clean(tokens.filter(_.is_proper))
- clean_tokens.reverse.find(_.is_name).map(_.content)
- }
-
def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
def body_files(syntax: Outer_Syntax, text: String): List[String] =
{
- val thy_load_commands = syntax.thy_load_commands
val spans = Thy_Syntax.parse_spans(syntax.scan(text))
- spans.iterator.map({
- case toks @ (tok :: _) if tok.is_command =>
- thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
- case Some((_, exts)) =>
- find_file(toks) match {
- case Some(file) =>
- if (exts.isEmpty) List(file)
- else exts.map(ext => file + "." + ext)
- case None => Nil
- }
- case None => Nil
- }
- case _ => Nil
- }).flatten.toList
+ spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
}
def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
{
val theory = Thy_Header.base_name(s)
- if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
+ if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
else {
val path = Path.explode(s)
- val node = append(master.dir, Thy_Load.thy_path(path))
- val dir = append(master.dir, path.dir)
- Document.Node.Name(node, dir, theory)
+ val node = append(master.master_dir, Thy_Load.thy_path(path))
+ val master_dir = append(master.master_dir, path.dir)
+ Document.Node.Name(node, master_dir, theory)
}
}
@@ -125,8 +99,11 @@
/* theory text edits */
- def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
- : (List[Document.Edit_Command], Document.Version) =
- Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
+ def text_edits(
+ reparse_limit: Int,
+ previous: Document.Version,
+ doc_blobs: Document.Blobs,
+ edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+ Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
}
--- a/src/Pure/Thy/thy_syntax.ML Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Wed Nov 20 16:43:09 2013 +0100
@@ -15,7 +15,7 @@
val span_content: span -> Token.T list
val present_span: span -> Output.output
val parse_spans: Token.T list -> span list
- val resolve_files: (string -> Path.T * Position.T -> Token.file list) -> span -> span
+ val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
datatype 'a element = Element of 'a * ('a element list * 'a) option
val atom: 'a -> 'a element
val map_element: ('a -> 'b) -> 'a element -> 'b element
--- a/src/Pure/Thy/thy_syntax.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Wed Nov 20 16:43:09 2013 +0100
@@ -33,7 +33,7 @@
def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
- List((0, node_name.theory, buffer()))
+ List((0, node_name.toString, buffer()))
@tailrec def close(level: Int => Boolean)
{
@@ -68,7 +68,7 @@
/* result structure */
val spans = parse_spans(syntax.scan(text))
- spans.foreach(span => add(Command(Document_ID.none, node_name, span, syntax.thy_load(span))))
+ spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
result()
}
}
@@ -225,23 +225,73 @@
}
+ /* inlined files */
+
+ private def find_file(tokens: List[Token]): Option[String] =
+ {
+ def clean(toks: List[Token]): List[Token] =
+ toks match {
+ case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
+ case t :: ts => t :: clean(ts)
+ case Nil => Nil
+ }
+ val clean_tokens = clean(tokens.filter(_.is_proper))
+ clean_tokens.reverse.find(_.is_name).map(_.content)
+ }
+
+ def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
+ syntax.thy_load(span) match {
+ case Some(exts) =>
+ find_file(span) match {
+ case Some(file) =>
+ if (exts.isEmpty) List(file)
+ else exts.map(ext => file + "." + ext)
+ case None => Nil
+ }
+ case None => Nil
+ }
+
+ def resolve_files(
+ thy_load: Thy_Load,
+ syntax: Outer_Syntax,
+ node_name: Document.Node.Name,
+ span: List[Token],
+ doc_blobs: Document.Blobs)
+ : List[Command.Blob] =
+ {
+ span_files(syntax, span).map(file =>
+ Exn.capture {
+ val name =
+ Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
+ (name, doc_blobs.get(name).map(_.sha1_digest))
+ }
+ )
+ }
+
+
/* reparse range of command spans */
@tailrec private def chop_common(
- cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
+ cmds: List[Command], spans: List[(List[Command.Blob], List[Token])])
+ : (List[Command], List[(List[Command.Blob], List[Token])]) =
(cmds, spans) match {
- case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
+ case (c :: cs, (blobs, span) :: ps) if c.blobs == blobs && c.span == span =>
+ chop_common(cs, ps)
case _ => (cmds, spans)
}
private def reparse_spans(
+ thy_load: Thy_Load,
syntax: Outer_Syntax,
+ doc_blobs: Document.Blobs,
name: Document.Node.Name,
commands: Linear_Set[Command],
first: Command, last: Command): Linear_Set[Command] =
{
val cmds0 = commands.iterator(first, last).toList
- val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
+ val spans0 =
+ parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
+ map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
val (cmds1, spans1) = chop_common(cmds0, spans0)
@@ -256,7 +306,7 @@
case cmd :: _ =>
val hook = commands.prev(cmd)
val inserted =
- spans2.map(span => Command(Document_ID.make(), name, span, syntax.thy_load(span)))
+ spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
(commands /: cmds2)(_ - _).append_after(hook, inserted)
}
}
@@ -266,7 +316,9 @@
// FIXME somewhat slow
private def recover_spans(
+ thy_load: Thy_Load,
syntax: Outer_Syntax,
+ doc_blobs: Document.Blobs,
name: Document.Node.Name,
perspective: Command.Perspective,
commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -282,7 +334,7 @@
case Some(first_unparsed) =>
val first = next_invisible_command(cmds.reverse, first_unparsed)
val last = next_invisible_command(cmds, first_unparsed)
- recover(reparse_spans(syntax, name, cmds, first, last))
+ recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last))
case None => cmds
}
recover(commands)
@@ -292,7 +344,9 @@
/* consolidate unfinished spans */
private def consolidate_spans(
+ thy_load: Thy_Load,
syntax: Outer_Syntax,
+ doc_blobs: Document.Blobs,
reparse_limit: Int,
name: Document.Node.Name,
perspective: Command.Perspective,
@@ -312,7 +366,7 @@
last = it.next
i += last.length
}
- reparse_spans(syntax, name, commands, first_unfinished, last)
+ reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last)
case None => commands
}
case None => commands
@@ -333,7 +387,11 @@
inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
}
- private def text_edit(syntax: Outer_Syntax, reparse_limit: Int,
+ private def text_edit(
+ thy_load: Thy_Load,
+ syntax: Outer_Syntax,
+ doc_blobs: Document.Blobs,
+ reparse_limit: Int,
node: Document.Node, edit: Document.Edit_Text): Document.Node =
{
edit match {
@@ -342,7 +400,8 @@
case (name, Document.Node.Edits(text_edits)) =>
val commands0 = node.commands
val commands1 = edit_text(text_edits, commands0)
- val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
+ val commands2 =
+ recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
node.update_commands(commands2)
case (_, Document.Node.Deps(_)) => node
@@ -354,46 +413,64 @@
if (node.same_perspective(perspective)) node
else
node.update_perspective(perspective).update_commands(
- consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
+ consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
+ name, visible, node.commands))
+
+ case (_, Document.Node.Blob()) => node
}
}
def text_edits(
- base_syntax: Outer_Syntax,
+ thy_load: Thy_Load,
reparse_limit: Int,
previous: Document.Version,
+ doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text])
: (List[Document.Edit_Command], Document.Version) =
{
- val (syntax, reparse, nodes0, doc_edits0) = header_edits(base_syntax, previous, edits)
- val reparse_set = reparse.toSet
-
- var nodes = nodes0
- val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+ val (syntax, reparse0, nodes0, doc_edits0) =
+ header_edits(thy_load.base_syntax, previous, edits)
- val node_edits =
- (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
- .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
+ if (edits.isEmpty)
+ (Nil, Document.Version.make(syntax, previous.nodes))
+ else {
+ val reparse =
+ (reparse0 /: nodes0.entries)({
+ case (reparse, (name, node)) =>
+ if (node.thy_load_commands.isEmpty) reparse
+ else name :: reparse
+ })
+ val reparse_set = reparse.toSet
- node_edits foreach {
- case (name, edits) =>
- val node = nodes(name)
- val commands = node.commands
+ var nodes = nodes0
+ val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+
+ val node_edits =
+ (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+ .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]] // FIXME ???
- val node1 =
- if (reparse_set(name) && !commands.isEmpty)
- node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
- else node
- val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
+ node_edits foreach {
+ case (name, edits) =>
+ val node = nodes(name)
+ val commands = node.commands
- if (!(node.same_perspective(node2.perspective)))
- doc_edits += (name -> node2.perspective)
-
- doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+ val node1 =
+ if (reparse_set(name) && !commands.isEmpty)
+ node.update_commands(
+ reparse_spans(thy_load, syntax, doc_blobs,
+ name, commands, commands.head, commands.last))
+ else node
+ val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _))
- nodes += (name -> node2)
+ if (!(node.same_perspective(node2.perspective)))
+ doc_edits += (name -> node2.perspective)
+
+ doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+
+ nodes += (name -> node2)
+ }
+
+ (doc_edits.toList, Document.Version.make(syntax, nodes))
}
-
- (doc_edits.toList, Document.Version.make(syntax, nodes))
}
}
--- a/src/Pure/Tools/build.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 20 16:43:09 2013 +0100
@@ -417,7 +417,8 @@
val parent = deps(parent_name)
(parent.loaded_theories, parent.syntax)
}
- val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
+ val thy_load = new Thy_Load(preloaded, parent_syntax)
+ val thy_info = new Thy_Info(thy_load)
if (verbose || list_files) {
val groups =
@@ -429,7 +430,7 @@
val thy_deps =
thy_info.dependencies(
info.theories.map(_._2).flatten.
- map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
+ map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
val loaded_theories = thy_deps.loaded_theories
val keywords = thy_deps.keywords
--- a/src/Tools/jEdit/src/document_model.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Wed Nov 20 16:43:09 2013 +0100
@@ -60,17 +60,23 @@
{
/* header */
+ def is_theory: Boolean = node_name.is_theory
+
def node_header(): Document.Node.Header =
{
Swing_Thread.require()
- JEdit_Lib.buffer_lock(buffer) {
- Exn.capture {
- PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
- } match {
- case Exn.Res(header) => header
- case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
+
+ if (is_theory) {
+ JEdit_Lib.buffer_lock(buffer) {
+ Exn.capture {
+ PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
+ } match {
+ case Exn.Res(header) => header
+ case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
+ }
}
}
+ else Document.Node.no_header
}
@@ -82,7 +88,7 @@
def node_required_=(b: Boolean)
{
Swing_Thread.require()
- if (_node_required != b) {
+ if (_node_required != b && is_theory) {
_node_required = b
PIDE.options_changed()
PIDE.editor.flush()
@@ -96,18 +102,51 @@
{
Swing_Thread.require()
- if (Isabelle.continuous_checking) {
+ if (Isabelle.continuous_checking && is_theory) {
val snapshot = this.snapshot()
- Document.Node.Perspective(node_required, Text.Perspective(
+
+ val document_view_ranges =
for {
doc_view <- PIDE.document_views(buffer)
range <- doc_view.perspective(snapshot).ranges
- } yield range), PIDE.editor.node_overlays(node_name))
+ } yield range
+
+ val thy_load_ranges =
+ for {
+ cmd <- snapshot.node.thy_load_commands
+ blob_name <- cmd.blobs_names
+ blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
+ if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
+ start <- snapshot.node.command_start(cmd)
+ range = snapshot.convert(cmd.proper_range + start)
+ } yield range
+
+ Document.Node.Perspective(node_required,
+ Text.Perspective(document_view_ranges ::: thy_load_ranges),
+ PIDE.editor.node_overlays(node_name))
}
else empty_perspective
}
+ /* blob */
+
+ private var _blob: Option[Bytes] = None // owned by Swing thread
+
+ private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
+
+ def blob(): Bytes =
+ Swing_Thread.require {
+ _blob match {
+ case Some(b) => b
+ case None =>
+ val b = PIDE.thy_load.file_content(buffer)
+ _blob = Some(b)
+ b
+ }
+ }
+
+
/* edits */
def init_edits(): List[Document.Edit_Text] =
@@ -118,10 +157,13 @@
val text = JEdit_Lib.buffer_text(buffer)
val perspective = node_perspective()
- List(session.header_edit(node_name, header),
- node_name -> Document.Node.Clear(),
- node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
- node_name -> perspective)
+ if (is_theory)
+ List(session.header_edit(node_name, header),
+ node_name -> Document.Node.Clear(),
+ node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
+ node_name -> perspective)
+ else
+ List(node_name -> Document.Node.Blob())
}
def node_edits(
@@ -131,16 +173,20 @@
{
Swing_Thread.require()
- val header_edit = session.header_edit(node_name, node_header())
- if (clear)
- List(header_edit,
- node_name -> Document.Node.Clear(),
- node_name -> Document.Node.Edits(text_edits),
- node_name -> perspective)
+ if (is_theory) {
+ val header_edit = session.header_edit(node_name, node_header())
+ if (clear)
+ List(header_edit,
+ node_name -> Document.Node.Clear(),
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
+ else
+ List(header_edit,
+ node_name -> Document.Node.Edits(text_edits),
+ node_name -> perspective)
+ }
else
- List(header_edit,
- node_name -> Document.Node.Edits(text_edits),
- node_name -> perspective)
+ List(node_name -> Document.Node.Blob())
}
@@ -170,6 +216,8 @@
def edit(clear: Boolean, e: Text.Edit)
{
+ reset_blob()
+
if (clear) {
pending_clear = true
pending.clear
--- a/src/Tools/jEdit/src/document_view.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Wed Nov 20 16:43:09 2013 +0100
@@ -82,7 +82,7 @@
PIDE.editor.current_command(view, snapshot) match {
case Some(command) =>
snapshot.node.command_start(command) match {
- case Some(start) => List(command.proper_range + start)
+ case Some(start) => List(snapshot.convert(command.proper_range + start))
case None => Nil
}
case None => Nil
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Nov 20 16:43:09 2013 +0100
@@ -133,15 +133,15 @@
class Isabelle_Sidekick_Default extends
- Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name)
+ Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
class Isabelle_Sidekick_Options extends
- Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy)
+ Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
class Isabelle_Sidekick_Root extends
- Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy)
+ Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Nov 20 16:43:09 2013 +0100
@@ -23,17 +23,8 @@
{
Swing_Thread.require()
- session.update(
- (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
- case (edits, buffer) =>
- JEdit_Lib.buffer_lock(buffer) {
- PIDE.document_model(buffer) match {
- case Some(model) => model.flushed_edits() ::: edits
- case None => edits
- }
- }
- }
- )
+ val edits = PIDE.document_models().flatMap(_.flushed_edits())
+ if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
}
private val delay_flush =
@@ -72,11 +63,13 @@
Swing_Thread.require()
val text_area = view.getTextArea
+ val buffer = view.getBuffer
+
PIDE.document_view(text_area) match {
case Some(doc_view) =>
val node = snapshot.version.nodes(doc_view.model.node_name)
val caret = snapshot.revert(text_area.getCaretPosition)
- if (caret < text_area.getBuffer.getLength) {
+ if (caret < buffer.getLength) {
val caret_commands = node.command_range(caret)
if (caret_commands.hasNext) {
val (cmd0, _) = caret_commands.next
@@ -85,7 +78,15 @@
else None
}
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
- case None => None
+ case None =>
+ PIDE.document_model(buffer) match {
+ case Some(model) if !model.is_theory =>
+ snapshot.version.nodes.thy_load_commands(model.node_name) match {
+ case cmd :: _ => Some(cmd)
+ case Nil => None
+ }
+ case _ => None
+ }
}
}
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Wed Nov 20 16:43:09 2013 +0100
@@ -9,26 +9,31 @@
import isabelle._
-import java.io.{File => JFile, IOException}
+import java.io.{File => JFile, IOException, ByteArrayOutputStream}
import javax.swing.text.Segment
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
import org.gjt.sp.jedit.MiscUtilities
import org.gjt.sp.jedit.{View, Buffer}
-
+import org.gjt.sp.jedit.bufferio.BufferIORequest
class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
extends Thy_Load(loaded_theories, base_syntax)
{
/* document node names */
- def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
- Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName))
+ def node_name(buffer: Buffer): Document.Node.Name =
+ {
+ val node = JEdit_Lib.buffer_name(buffer)
+ val theory = Thy_Header.thy_name(node).getOrElse("")
+ val master_dir = if (theory == "") "" else buffer.getDirectory
+ Document.Node.Name(node, master_dir, theory)
+ }
- def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+ def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
{
- val name = JEdit_Lib.buffer_name(buffer)
- Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+ val name = node_name(buffer)
+ if (name.is_theory) Some(name) else None
}
@@ -37,7 +42,7 @@
override def append(dir: String, source_path: Path): String =
{
val path = source_path.expand
- if (path.is_absolute) Isabelle_System.platform_path(path)
+ if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
else {
val vfs = VFSManager.getVFSForPath(dir)
if (vfs.isInstanceOf[FileVFS])
@@ -83,5 +88,28 @@
catch { case _: IOException => }
}
}
+
+
+ /* file content */
+
+ def file_content(buffer: Buffer): Bytes =
+ {
+ val path = buffer.getPath
+ val vfs = VFSManager.getVFSForPath(path)
+ val content =
+ new BufferIORequest(null, buffer, null, vfs, path) {
+ def _run() { }
+ def apply(): Bytes =
+ {
+ val out =
+ new ByteArrayOutputStream(buffer.getLength + 1) {
+ def content(): Bytes = Bytes(this.buf, 0, this.count)
+ }
+ write(buffer, out)
+ out.content()
+ }
+ }
+ content()
+ }
}
--- a/src/Tools/jEdit/src/plugin.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Nov 20 16:43:09 2013 +0100
@@ -73,9 +73,17 @@
def document_views(buffer: Buffer): List[Document_View] =
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
- doc_view = document_view(text_area)
- if doc_view.isDefined
- } yield doc_view.get
+ doc_view <- document_view(text_area)
+ } yield doc_view
+
+ def document_models(): List[Document_Model] =
+ for {
+ buffer <- JEdit_Lib.jedit_buffers().toList
+ model <- document_model(buffer)
+ } yield model
+
+ def document_blobs(): Document.Blobs =
+ document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
def exit_models(buffers: List[Buffer])
{
@@ -96,27 +104,24 @@
val init_edits =
(List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
JEdit_Lib.buffer_lock(buffer) {
- val (model_edits, opt_model) =
- thy_load.buffer_node_name(buffer) match {
- case Some(node_name) =>
- document_model(buffer) match {
- case Some(model) if model.node_name == node_name => (Nil, Some(model))
- case _ =>
- val model = Document_Model.init(session, buffer, node_name)
- (model.init_edits(), Some(model))
- }
- case None => (Nil, None)
+ val node_name = thy_load.node_name(buffer)
+ val (model_edits, model) =
+ document_model(buffer) match {
+ case Some(model) if model.node_name == node_name => (Nil, model)
+ case _ =>
+ val model = Document_Model.init(session, buffer, node_name)
+ (model.init_edits(), model)
}
- if (opt_model.isDefined) {
+ if (model.is_theory) {
for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
- if (document_view(text_area).map(_.model) != opt_model)
- Document_View.init(opt_model.get, text_area)
+ if (document_view(text_area).map(_.model) != Some(model))
+ Document_View.init(model, text_area)
}
}
model_edits ::: edits
}
}
- session.update(init_edits)
+ session.update(document_blobs(), init_edits)
}
}
@@ -124,8 +129,8 @@
{
JEdit_Lib.swing_buffer_lock(buffer) {
document_model(buffer) match {
- case Some(model) => Document_View.init(model, text_area)
- case None =>
+ case Some(model) if model.is_theory => Document_View.init(model, text_area)
+ case _ =>
}
}
}
@@ -163,8 +168,11 @@
buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
val thys =
- for (buffer <- buffers; model <- PIDE.document_model(buffer))
- yield model.node_name
+ for {
+ buffer <- buffers
+ model <- PIDE.document_model(buffer)
+ if model.is_theory
+ } yield model.node_name
val thy_info = new Thy_Info(PIDE.thy_load)
// FIXME avoid I/O in Swing thread!?!
--- a/src/Tools/jEdit/src/rendering.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Wed Nov 20 16:43:09 2013 +0100
@@ -226,7 +226,7 @@
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
- val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+ val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
val link = PIDE.editor.hyperlink_file(jedit_file)
Some(Text.Info(snapshot.convert(info_range), link) :: links)
@@ -369,7 +369,7 @@
Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
- val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+ val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
if name == Markup.SORTING || name == Markup.TYPING =>
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Nov 20 16:43:09 2013 +0100
@@ -186,10 +186,10 @@
val snapshot = PIDE.session.snapshot()
val iterator =
- restriction match {
+ (restriction match {
case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
case None => snapshot.version.nodes.entries
- }
+ }).filter(_._1.is_theory)
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
if (PIDE.thy_load.loaded_theories(name.theory)) status