--- a/src/Pure/Isar/outer_syntax.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Tue Aug 07 15:01:48 2012 +0200
@@ -60,14 +60,10 @@
def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
- def add_keywords(header: Document.Node_Header): Outer_Syntax =
- header match {
- case Exn.Res(deps) =>
- (this /: deps.keywords) {
- case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
- case (syntax, ((name, None))) => syntax + name
- }
- case Exn.Exn(_) => this
+ def add_keywords(header: Document.Node.Header): Outer_Syntax =
+ (this /: header.keywords) {
+ case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
+ case (syntax, ((name, None))) => syntax + name
}
def is_command(name: String): Boolean =
--- a/src/Pure/PIDE/document.ML Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 07 15:01:48 2012 +0200
@@ -15,11 +15,11 @@
val new_id: unit -> id
val parse_id: string -> id
val print_id: id -> string
- type node_header = (string * Thy_Header.header) Exn.result
+ type node_header = string * Thy_Header.header * string list
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
- Header of node_header |
+ Deps of node_header |
Perspective of command_id list
type edit = string * node_edit
type state
@@ -59,7 +59,7 @@
(** document structure **)
-type node_header = (string * Thy_Header.header) Exn.result;
+type node_header = string * Thy_Header.header * string list;
type perspective = (command_id -> bool) * command_id option;
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
@@ -67,7 +67,7 @@
val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
abstype node = Node of
- {header: node_header,
+ {header: node_header, (*master directory, theory header, errors*)
perspective: perspective, (*visible commands, last*)
entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*)
result: exec option} (*result of last execution*)
@@ -83,7 +83,7 @@
fun make_perspective command_ids : perspective =
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
-val no_header = Exn.Exn (ERROR "Bad theory header");
+val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
val no_perspective = make_perspective [];
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
@@ -92,7 +92,10 @@
(* basic components *)
-fun get_header (Node {header, ...}) = header;
+fun get_header (Node {header = (master, header, errors), ...}) =
+ if null errors then (master, header)
+ else error (cat_lines errors);
+
fun set_header header =
map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
@@ -128,7 +131,7 @@
datatype node_edit =
Clear |
Edits of (command_id option * command_id option) list |
- Header of node_header |
+ Deps of node_header |
Perspective of command_id list;
type edit = string * node_edit;
@@ -178,22 +181,21 @@
(case node_edit of
Clear => update_node name clear_node nodes
| Edits edits => update_node name (edit_node edits) nodes
- | Header header =>
+ | Deps (master, header, errors) =>
let
- val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
- val header' =
- ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
- handle exn as ERROR _ => Exn.Exn exn;
+ val errors1 =
+ (Thy_Header.define_keywords header; errors)
+ handle ERROR msg => errors @ [msg];
val nodes1 = nodes
|> default_node name
- |> fold default_node imports;
+ |> fold default_node (#imports header);
val nodes2 = nodes1
|> Graph.Keys.fold
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
- val (header'', nodes3) =
- (header', Graph.add_deps_acyclic (name, imports) nodes2)
- handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
- in Graph.map_node name (set_header header'') nodes3 end
+ val (nodes3, errors2) =
+ (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
+ handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
+ in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
| Perspective perspective => update_node name (set_perspective perspective) nodes);
fun put_node (name, node) (Version nodes) =
@@ -374,7 +376,7 @@
fun init_theory imports node =
let
(* FIXME provide files via Scala layer, not master_dir *)
- val (dir, header) = Exn.release (get_header node);
+ val (dir, header) = get_header node;
val master_dir =
(case Url.explode dir of
Url.File path => path
@@ -393,7 +395,7 @@
fun check_theory full name node =
is_some (Thy_Info.lookup_theory name) orelse
- is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
+ can get_header node andalso (not full orelse is_some (get_result node));
fun last_common state last_visible node0 node =
let
--- a/src/Pure/PIDE/document.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 07 15:01:48 2012 +0200
@@ -35,14 +35,18 @@
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
- type Node_Header = Exn.Result[Node.Deps]
-
object Node
{
- sealed case class Deps(
+ sealed case class Header(
imports: List[Name],
keywords: Thy_Header.Keywords,
- uses: List[(String, Boolean)])
+ uses: List[(String, Boolean)],
+ errors: List[String] = Nil)
+ {
+ def error(msg: String): Header = copy(errors = errors ::: List(msg))
+ }
+
+ def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
object Name
{
@@ -83,7 +87,7 @@
}
case class Clear[A, B]() extends Edit[A, B]
case class Edits[A, B](edits: List[A]) extends Edit[A, B]
- case class Header[A, B](header: Node_Header) extends Edit[A, B]
+ case class Deps[A, B](header: Header) extends Edit[A, B]
case class Perspective[A, B](perspective: B) extends Edit[A, B]
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
@@ -103,14 +107,14 @@
}
final class Node private(
- val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
+ val header: Node.Header = Node.bad_header("Bad theory header"),
val perspective: Command.Perspective = Command.Perspective.empty,
val blobs: Map[String, Blob] = Map.empty,
val commands: Linear_Set[Command] = Linear_Set.empty)
{
def clear: Node = new Node(header = header)
- def update_header(new_header: Node_Header): Node =
+ def update_header(new_header: Node.Header): Node =
new Node(new_header, perspective, blobs, commands)
def update_perspective(new_perspective: Command.Perspective): Node =
@@ -122,12 +126,6 @@
def update_commands(new_commands: Linear_Set[Command]): Node =
new Node(header, perspective, blobs, new_commands)
- def imports: List[Node.Name] =
- header match { case Exn.Res(deps) => deps.imports case _ => Nil }
-
- def keywords: Thy_Header.Keywords =
- header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
-
/* commands */
@@ -190,7 +188,7 @@
def + (entry: (Node.Name, Node)): Nodes =
{
val (name, node) = entry
- val imports = node.imports
+ val imports = node.header.imports
val graph1 =
(graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
--- a/src/Pure/PIDE/protocol.ML Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Tue Aug 07 15:01:48 2012 +0200
@@ -37,16 +37,15 @@
fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
fn ([], a) =>
let
- val ((((master, name), imports), keywords), uses) =
- pair (pair (pair (pair string string) (list string))
- (list (pair string (option (pair string (list string))))))
- (list (pair string bool)) a;
- val res =
- Exn.capture (fn () =>
- (master, Thy_Header.make name imports keywords
- (map (apfst Path.explode) uses))) ();
- in Document.Header res end,
- fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+ val (master, (name, (imports, (keywords, (uses, errors))))) =
+ pair string (pair string (pair (list string)
+ (pair (list (pair string (option (pair string (list string)))))
+ (pair (list (pair string bool)) (list string))))) a;
+ val (uses', errors') =
+ (map (apfst Path.explode) uses, errors)
+ handle ERROR msg => ([], errors @ [msg]);
+ val header = Thy_Header.make name imports keywords uses';
+ in Document.Deps (master, header, errors') end,
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
--- a/src/Pure/PIDE/protocol.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue Aug 07 15:01:48 2012 +0200
@@ -215,17 +215,16 @@
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) },
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
- { case Document.Node.Header(Exn.Res(deps)) =>
+ { case Document.Node.Deps(header) =>
val dir = Isabelle_System.posix_path(name.dir)
- val imports = deps.imports.map(_.node)
+ val imports = header.imports.map(_.node)
// FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
- val uses = deps.uses
+ val uses = header.uses
(Nil,
- pair(pair(pair(pair(Encode.string, Encode.string), list(Encode.string)),
- list(pair(Encode.string, option(pair(Encode.string, list(Encode.string)))))),
- list(pair(Encode.string, bool)))(
- (((dir, name.theory), imports), deps.keywords), uses)) },
- { case Document.Node.Header(Exn.Exn(e)) => (List(encode(Exn.message(e))), Nil) },
+ pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
+ pair(list(pair(Encode.string, option(pair(Encode.string, list(Encode.string))))),
+ pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
+ (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
--- a/src/Pure/System/build.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/System/build.scala Tue Aug 07 15:01:48 2012 +0200
@@ -363,12 +363,7 @@
val all_files =
thy_deps.map({ case (n, h) =>
val thy = Path.explode(n.node).expand
- val uses =
- h match {
- case Exn.Res(d) =>
- d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
- case _ => Nil
- }
+ val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
thy :: uses
}).flatten ::: info.files.map(file => info.dir + file)
val sources =
--- a/src/Pure/System/session.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/System/session.scala Tue Aug 07 15:01:48 2012 +0200
@@ -160,15 +160,13 @@
/* theory files */
- def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
+ def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
{
- val header1: Document.Node_Header =
- header match {
- case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
- Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
- case _ => header
- }
- (name, Document.Node.Header(header1))
+ val header1 =
+ if (thy_load.is_loaded(name.theory))
+ header.error("Attempt to update loaded theory " + quote(name.theory))
+ else header
+ (name, Document.Node.Deps(header1))
}
@@ -456,7 +454,7 @@
{ session_actor !? Edit(edits) }
def init_node(name: Document.Node.Name,
- header: Document.Node_Header, perspective: Text.Perspective, text: String)
+ header: Document.Node.Header, perspective: Text.Perspective, text: String)
{
edit(List(header_edit(name, header),
name -> Document.Node.Clear(), // FIXME diff wrt. existing node
@@ -465,7 +463,7 @@
}
def edit_node(name: Document.Node.Name,
- header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
+ header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
{
edit(List(header_edit(name, header),
name -> Document.Node.Edits(text_edits),
--- a/src/Pure/Thy/thy_header.ML Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML Tue Aug 07 15:01:48 2012 +0200
@@ -7,7 +7,8 @@
signature THY_HEADER =
sig
type header =
- {name: string, imports: string list,
+ {name: string,
+ imports: string list,
keywords: (string * Keyword.spec option) list,
uses: (Path.T * bool) list}
val make: string -> string list -> (string * Keyword.spec option) list ->
@@ -23,7 +24,8 @@
struct
type header =
- {name: string, imports: string list,
+ {name: string,
+ imports: string list,
keywords: (string * Keyword.spec option) list,
uses: (Path.T * bool) list};
--- a/src/Pure/Thy/thy_info.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala Tue Aug 07 15:01:48 2012 +0200
@@ -24,7 +24,7 @@
/* dependencies */
- type Dep = (Document.Node.Name, Document.Node_Header)
+ type Dep = (Document.Node.Name, Document.Node.Header)
private type Required = (List[Dep], Set[Document.Node.Name])
private def require_thys(initiators: List[Document.Node.Name],
@@ -40,7 +40,7 @@
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
- val node_deps =
+ val header =
try { thy_load.check_thy(name) }
catch {
case ERROR(msg) =>
@@ -48,10 +48,13 @@
quote(name.theory) + required_by(initiators))
}
val (deps1, seen1) =
- require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
- ((name, Exn.Res(node_deps)) :: deps1, seen1)
+ require_thys(name :: initiators, (deps, seen + name), header.imports)
+ ((name, header) :: deps1, seen1)
}
- catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
+ catch {
+ case e: Throwable =>
+ ((name, Document.Node.bad_header(Exn.message(e))) :: deps, seen + name)
+ }
}
}
--- a/src/Pure/Thy/thy_load.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala Tue Aug 07 15:01:48 2012 +0200
@@ -60,7 +60,7 @@
}
}
- def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps =
+ def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header =
{
val name1 = header.name
val imports = header.imports.map(import_name(name.dir, _))
@@ -69,10 +69,10 @@
if (name.theory != name1)
error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
" for theory " + quote(name1))
- Document.Node.Deps(imports, header.keywords, uses)
+ Document.Node.Header(imports, header.keywords, uses)
}
- def check_thy(name: Document.Node.Name): Document.Node.Deps =
+ def check_thy(name: Document.Node.Name): Document.Node.Header =
check_header(name, read_header(name))
}
--- a/src/Pure/Thy/thy_syntax.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Tue Aug 07 15:01:48 2012 +0200
@@ -134,19 +134,16 @@
val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
edits foreach {
- case (name, Document.Node.Header(header)) =>
+ case (name, Document.Node.Deps(header)) =>
val node = nodes(name)
val update_header =
- (node.header, header) match {
- case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
- case _ => true
- }
+ !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
if (update_header) {
val node1 = node.update_header(header)
- updated_imports = updated_imports || (node.imports != node1.imports)
- updated_keywords = updated_keywords || (node.keywords != node1.keywords)
+ updated_imports = updated_imports || (node.header.imports != node1.header.imports)
+ updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
nodes += (name -> node1)
- doc_edits += (name -> Document.Node.Header(header))
+ doc_edits += (name -> Document.Node.Deps(header))
}
case _ =>
}
@@ -289,7 +286,7 @@
doc_edits += (name -> Document.Node.Edits(cmd_edits))
nodes += (name -> node.update_commands(commands3))
- case (name, Document.Node.Header(_)) =>
+ case (name, Document.Node.Deps(_)) =>
case (name, Document.Node.Perspective(text_perspective)) =>
val node = nodes(name)
--- a/src/Tools/jEdit/src/document_model.scala Tue Aug 07 13:21:29 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Tue Aug 07 15:01:48 2012 +0200
@@ -63,13 +63,16 @@
{
/* header */
- def node_header(): Document.Node_Header =
+ def node_header(): Document.Node.Header =
{
Swing_Thread.require()
Isabelle.buffer_lock(buffer) {
Exn.capture {
Isabelle.thy_load.check_header(name,
Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
+ } match {
+ case Exn.Res(header) => header
+ case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
}
}
}