# HG changeset patch # User wenzelm # Date 1344344508 -7200 # Node ID ba531af9114879f0e2d87482bcae307bc22b055d # Parent e2b512024eab208354b61456e085570590d52733 simplified Document.Node.Header -- internalized errors; diff -r e2b512024eab -r ba531af91148 src/Pure/Isar/outer_syntax.scala --- 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 = diff -r e2b512024eab -r ba531af91148 src/Pure/PIDE/document.ML --- 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 diff -r e2b512024eab -r ba531af91148 src/Pure/PIDE/document.scala --- 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)) diff -r e2b512024eab -r ba531af91148 src/Pure/PIDE/protocol.ML --- 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; diff -r e2b512024eab -r ba531af91148 src/Pure/PIDE/protocol.scala --- 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) => { diff -r e2b512024eab -r ba531af91148 src/Pure/System/build.scala --- 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 = diff -r e2b512024eab -r ba531af91148 src/Pure/System/session.scala --- 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), diff -r e2b512024eab -r ba531af91148 src/Pure/Thy/thy_header.ML --- 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}; diff -r e2b512024eab -r ba531af91148 src/Pure/Thy/thy_info.scala --- 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) + } } } diff -r e2b512024eab -r ba531af91148 src/Pure/Thy/thy_load.scala --- 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)) } diff -r e2b512024eab -r ba531af91148 src/Pure/Thy/thy_syntax.scala --- 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) diff -r e2b512024eab -r ba531af91148 src/Tools/jEdit/src/document_model.scala --- 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)) } } }