provide node header via Scala layer;
authorwenzelm
Sat Aug 13 20:20:36 2011 +0200 (2011-08-13)
changeset 4418505641edb5d30
parent 44184 49501dc1a7b8
child 44186 806f0ec1a43d
provide node header via Scala layer;
clarified node edit Clear: retain header information;
run_command: node info via document model, error handling within transaction;
node names without ".thy" suffix, to coincide with traditional theory loader treatment;
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/ROOT.ML
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 16:07:26 2011 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:20:36 2011 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    val thread: bool -> (unit -> unit) -> Thread.thread
     1.5    type transition
     1.6    val empty: transition
     1.7 -  val init_of: transition -> string option
     1.8 +  val is_init: transition -> bool
     1.9    val print_of: transition -> bool
    1.10    val name_of: transition -> string
    1.11    val pos_of: transition -> Position.T
    1.12 @@ -356,7 +356,8 @@
    1.13  fun get_init (Transition {trans = [Init args], ...}) = SOME args
    1.14    | get_init _ = NONE;
    1.15  
    1.16 -val init_of = Option.map #2 o get_init;
    1.17 +val is_init = is_some o get_init;
    1.18 +
    1.19  fun print_of (Transition {print, ...}) = print;
    1.20  fun name_of (Transition {name, ...}) = name;
    1.21  fun pos_of (Transition {pos, ...}) = pos;
     2.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 13 16:07:26 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 13 20:20:36 2011 +0200
     2.3 @@ -15,9 +15,9 @@
     2.4    val new_id: unit -> id
     2.5    val parse_id: string -> id
     2.6    val print_id: id -> string
     2.7 -  type node_header = (string * string list * string list) Exn.result
     2.8 +  type node_header = (string * string list * (string * bool) list) Exn.result
     2.9    datatype node_edit =
    2.10 -    Remove |
    2.11 +    Clear |
    2.12      Edits of (command_id option * command_id option) list |
    2.13      Header of node_header
    2.14    type edit = string * node_edit
    2.15 @@ -55,7 +55,7 @@
    2.16  
    2.17  (** document structure **)
    2.18  
    2.19 -type node_header = (string * string list * string list) Exn.result;
    2.20 +type node_header = (string * string list * (string * bool) list) Exn.result;
    2.21  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    2.22  
    2.23  abstype node = Node of
    2.24 @@ -82,13 +82,17 @@
    2.25  fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
    2.26  
    2.27  val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
    2.28 -val empty_version = Version Graph.empty;
    2.29 +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id));
    2.30 +
    2.31 +fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    2.32 +fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
    2.33 +fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
    2.34  
    2.35  
    2.36  (* node edits and associated executions *)
    2.37  
    2.38  datatype node_edit =
    2.39 -  Remove |
    2.40 +  Clear |
    2.41    Edits of (command_id option * command_id option) list |
    2.42    Header of node_header;
    2.43  
    2.44 @@ -114,22 +118,30 @@
    2.45  
    2.46  (* version operations *)
    2.47  
    2.48 +val empty_version = Version Graph.empty;
    2.49 +
    2.50  fun nodes_of (Version nodes) = nodes;
    2.51 +val node_of = get_node o nodes_of;
    2.52  val node_names_of = Graph.keys o nodes_of;
    2.53  
    2.54 -fun get_node version name = Graph.get_node (nodes_of version) name
    2.55 -  handle Graph.UNDEF _ => empty_node;
    2.56 -
    2.57 -fun update_node name f =
    2.58 -  Graph.default_node (name, empty_node) #> Graph.map_node name f;
    2.59 +fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    2.60  
    2.61  fun edit_nodes (name, node_edit) (Version nodes) =
    2.62    Version
    2.63      (case node_edit of
    2.64 -      Remove => perhaps (try (Graph.del_node name)) nodes
    2.65 +      Clear => update_node name clear_node nodes
    2.66      | Edits edits => update_node name (edit_node edits) nodes
    2.67 -    (* FIXME maintain deps; cycles!? *)
    2.68 -    | Header header => update_node name (set_header header) nodes);
    2.69 +    | Header header =>
    2.70 +        let
    2.71 +          val node = get_node nodes name;
    2.72 +          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    2.73 +          val parents =
    2.74 +            (case header of Exn.Res (_, parents, _) => parents | _ => [])
    2.75 +            |> filter (can (Graph.get_node nodes'));
    2.76 +          val (header', nodes'') =
    2.77 +            (header, Graph.add_deps_acyclic (name, parents) nodes')
    2.78 +              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
    2.79 +        in Graph.map_node name (set_header header') nodes'' end);
    2.80  
    2.81  fun put_node name node (Version nodes) =
    2.82    Version (nodes
    2.83 @@ -214,11 +226,11 @@
    2.84  
    2.85  fun get_theory state version_id pos name =
    2.86    let
    2.87 -    val last = get_last (get_node (the_version state version_id) name);
    2.88 +    val last = get_last (node_of (the_version state version_id) name);
    2.89      val st =
    2.90        (case Lazy.peek (the_exec state last) of
    2.91          SOME result => #2 (Exn.release result)
    2.92 -      | NONE => error ("Unfinished execution for theory " ^ quote name));
    2.93 +      | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
    2.94    in Toplevel.end_theory pos st end;
    2.95  
    2.96  
    2.97 @@ -263,41 +275,38 @@
    2.98  
    2.99  in
   2.100  
   2.101 -fun run_command node_name raw_tr st =
   2.102 -  (case
   2.103 -      (case Toplevel.init_of raw_tr of
   2.104 -        SOME _ =>
   2.105 -          Exn.capture (fn () =>
   2.106 -            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
   2.107 -            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
   2.108 -      | NONE => Exn.Res raw_tr) of
   2.109 -    Exn.Res tr =>
   2.110 -      let
   2.111 -        val is_init = is_some (Toplevel.init_of tr);
   2.112 -        val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   2.113 -        val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   2.114 +fun run_command (node_name, node_header) raw_tr st =
   2.115 +  let
   2.116 +    val is_init = Toplevel.is_init raw_tr;
   2.117 +    val tr =
   2.118 +      if is_init then
   2.119 +        raw_tr |> Toplevel.modify_init (fn _ =>
   2.120 +          let
   2.121 +            (* FIXME get theories from document state *)
   2.122 +            (* FIXME provide files via Scala layer *)
   2.123 +            val (name, imports, uses) = Exn.release node_header;
   2.124 +            val master = SOME (Path.dir (Path.explode node_name));
   2.125 +          in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
   2.126 +      else raw_tr;
   2.127  
   2.128 -        val start = Timing.start ();
   2.129 -        val (errs, result) =
   2.130 -          if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   2.131 -          else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   2.132 -        val _ = timing tr (Timing.result start);
   2.133 -        val _ = List.app (Toplevel.error_msg tr) errs;
   2.134 -        val res =
   2.135 -          (case result of
   2.136 -            NONE => (Toplevel.status tr Markup.failed; (false, st))
   2.137 -          | SOME st' =>
   2.138 -             (Toplevel.status tr Markup.finished;
   2.139 -              proof_status tr st';
   2.140 -              if do_print then async_state tr st' else ();
   2.141 -              (true, st')));
   2.142 -      in res end
   2.143 -  | Exn.Exn exn =>
   2.144 -      if Exn.is_interrupt exn then reraise exn
   2.145 -      else
   2.146 -       (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
   2.147 -        Toplevel.status raw_tr Markup.failed;
   2.148 -        (false, Toplevel.toplevel)));
   2.149 +    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   2.150 +    val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   2.151 +
   2.152 +    val start = Timing.start ();
   2.153 +    val (errs, result) =
   2.154 +      if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   2.155 +      else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   2.156 +    val _ = timing tr (Timing.result start);
   2.157 +    val _ = List.app (Toplevel.error_msg tr) errs;
   2.158 +  in
   2.159 +    (case result of
   2.160 +      NONE => (Toplevel.status tr Markup.failed; (false, st))
   2.161 +    | SOME st' =>
   2.162 +       (Toplevel.status tr Markup.finished;
   2.163 +        proof_status tr st';
   2.164 +        if do_print then async_state tr st' else ();
   2.165 +        (true, st')))
   2.166 +  end;
   2.167  
   2.168  end;
   2.169  
   2.170 @@ -315,7 +324,7 @@
   2.171      NONE => true
   2.172    | SOME exec' => exec' <> exec);
   2.173  
   2.174 -fun new_exec name (id: command_id) (exec_id, updates, state) =
   2.175 +fun new_exec node_info (id: command_id) (exec_id, updates, state) =
   2.176    let
   2.177      val exec = the_exec state exec_id;
   2.178      val exec_id' = new_id ();
   2.179 @@ -325,7 +334,7 @@
   2.180          let
   2.181            val st = #2 (Lazy.force exec);
   2.182            val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
   2.183 -        in run_command name exec_tr st end);
   2.184 +        in run_command node_info exec_tr st end);
   2.185      val state' = define_exec exec_id' exec' state;
   2.186    in (exec_id', (id, exec_id') :: updates, state') end;
   2.187  
   2.188 @@ -338,8 +347,11 @@
   2.189      val new_version = fold edit_nodes edits old_version;
   2.190  
   2.191      fun update_node name (rev_updates, version, st) =
   2.192 -      let val node = get_node version name in
   2.193 -        (case first_entry NONE (is_changed (get_node old_version name)) node of
   2.194 +      let
   2.195 +        val node = node_of version name;
   2.196 +        val header = get_header node;
   2.197 +      in
   2.198 +        (case first_entry NONE (is_changed (node_of old_version name)) node of
   2.199            NONE => (rev_updates, version, st)
   2.200          | SOME ((prev, id), _) =>
   2.201              let
   2.202 @@ -348,12 +360,12 @@
   2.203                    NONE => no_id
   2.204                  | SOME prev_id => the_default no_id (the_entry node prev_id));
   2.205                val (last, rev_upds, st') =
   2.206 -                fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   2.207 +                fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st);
   2.208                val node' = node |> fold update_entry rev_upds |> set_last last;
   2.209              in (rev_upds @ rev_updates, put_node name node' version, st') end)
   2.210        end;
   2.211  
   2.212 -    (* FIXME proper node deps *)
   2.213 +    (* FIXME Graph.schedule *)
   2.214      val (rev_updates, new_version', state') =
   2.215        fold update_node (node_names_of new_version) ([], new_version, state);
   2.216      val state'' = define_version new_id new_version' state';
   2.217 @@ -380,7 +392,7 @@
   2.218            [fn () =>
   2.219              node_names_of version |> List.app (fn name =>
   2.220                fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
   2.221 -                  (get_node version name) ())];
   2.222 +                  (node_of version name) ())];
   2.223  
   2.224      in (versions, commands, execs, execution') end);
   2.225  
     3.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 13 16:07:26 2011 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 13 20:20:36 2011 +0200
     3.3 @@ -44,12 +44,12 @@
     3.4      {
     3.5        def map[B](f: A => B): Edit[B] =
     3.6          this match {
     3.7 -          case Remove() => Remove()
     3.8 +          case Clear() => Clear()
     3.9            case Edits(es) => Edits(es.map(f))
    3.10            case Header(header) => Header(header)
    3.11          }
    3.12      }
    3.13 -    case class Remove[A]() extends Edit[A]
    3.14 +    case class Clear[A]() extends Edit[A]
    3.15      case class Edits[A](edits: List[A]) extends Edit[A]
    3.16      case class Header[A](header: Node_Header) extends Edit[A]
    3.17  
     4.1 --- a/src/Pure/PIDE/isar_document.ML	Sat Aug 13 16:07:26 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.ML	Sat Aug 13 20:20:36 2011 +0200
     4.3 @@ -22,10 +22,11 @@
     4.4              let open XML.Decode in
     4.5                list (pair string
     4.6                  (variant
     4.7 -                 [fn ([], []) => Document.Remove,
     4.8 +                 [fn ([], []) => Document.Clear,
     4.9                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    4.10                    fn ([], a) =>
    4.11 -                    Document.Header (Exn.Res (triple string (list string) (list string) a)),
    4.12 +                    Document.Header
    4.13 +                      (Exn.Res (triple string (list string) (list (pair string bool)) a)),
    4.14                    fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
    4.15              end;
    4.16  
     5.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Aug 13 16:07:26 2011 +0200
     5.2 +++ b/src/Pure/PIDE/isar_document.scala	Sat Aug 13 20:20:36 2011 +0200
     5.3 @@ -147,10 +147,10 @@
     5.4        def encode: T[List[Document.Edit_Command_ID]] =
     5.5          list(pair(string,
     5.6            variant(List(
     5.7 -            { case Document.Node.Remove() => (Nil, Nil) },
     5.8 +            { case Document.Node.Clear() => (Nil, Nil) },
     5.9              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
    5.10              { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    5.11 -                (Nil, triple(string, list(string), list(string))(a, b, c)) },
    5.12 +                (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
    5.13              { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
    5.14        YXML.string_of_body(encode(edits)) }
    5.15  
     6.1 --- a/src/Pure/ROOT.ML	Sat Aug 13 16:07:26 2011 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Sat Aug 13 20:20:36 2011 +0200
     6.3 @@ -243,10 +243,10 @@
     6.4  use "Thy/thy_output.ML";
     6.5  use "Thy/thy_syntax.ML";
     6.6  use "Isar/outer_syntax.ML";
     6.7 -use "PIDE/document.ML";
     6.8  use "Thy/present.ML";
     6.9  use "Thy/thy_load.ML";
    6.10  use "Thy/thy_info.ML";
    6.11 +use "PIDE/document.ML";
    6.12  use "Thy/rail.ML";
    6.13  
    6.14  (*theory and proof operations*)
     7.1 --- a/src/Pure/System/session.scala	Sat Aug 13 16:07:26 2011 +0200
     7.2 +++ b/src/Pure/System/session.scala	Sat Aug 13 20:20:36 2011 +0200
     7.3 @@ -188,13 +188,14 @@
     7.4      {
     7.5        val syntax = current_syntax()
     7.6        val previous = global_state().history.tip.version
     7.7 +
     7.8        val norm_header =
     7.9          Document.Node.norm_header[Text.Edit](
    7.10            name => file_store.append(master_dir, Path.explode(name)), header)
    7.11 -      val doc_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    7.12 -      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    7.13 +      val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    7.14 +      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
    7.15        val change =
    7.16 -        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
    7.17 +        global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
    7.18  
    7.19        result.map {
    7.20          case (doc_edits, _) =>
    7.21 @@ -331,7 +332,7 @@
    7.22          case Init_Node(name, master_dir, header, text) if prover.isDefined =>
    7.23            // FIXME compare with existing node
    7.24            handle_edits(name, master_dir, header,
    7.25 -            List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
    7.26 +            List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
    7.27            reply(())
    7.28  
    7.29          case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
     8.1 --- a/src/Pure/Thy/thy_header.scala	Sat Aug 13 16:07:26 2011 +0200
     8.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Aug 13 20:20:36 2011 +0200
     8.3 @@ -28,10 +28,10 @@
     8.4  
     8.5    /* theory file name */
     8.6  
     8.7 -  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
     8.8 +  private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""")
     8.9  
    8.10 -  def thy_name(s: String): Option[String] =
    8.11 -    s match { case Thy_Name(name) => Some(name) case _ => None }
    8.12 +  def thy_name(s: String): Option[(String, String)] =
    8.13 +    s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None }
    8.14  
    8.15    def thy_path(name: String): Path = Path.basic(name).ext("thy")
    8.16  
    8.17 @@ -44,7 +44,8 @@
    8.18      val theory_name = atom("theory name", _.is_name)
    8.19  
    8.20      val file =
    8.21 -      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name
    8.22 +      keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
    8.23 +      file_name ^^ (x => (x, true))
    8.24  
    8.25      val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs }
    8.26  
    8.27 @@ -106,12 +107,13 @@
    8.28  }
    8.29  
    8.30  
    8.31 -sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
    8.32 +sealed case class Thy_Header(
    8.33 +  val name: String, val imports: List[String], val uses: List[(String, Boolean)])
    8.34  {
    8.35    def map(f: String => String): Thy_Header =
    8.36 -    Thy_Header(f(name), imports.map(f), uses.map(f))
    8.37 +    Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
    8.38  
    8.39    def norm_deps(f: String => String): Thy_Header =
    8.40 -    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
    8.41 +    copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2)))
    8.42  }
    8.43  
     9.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 16:07:26 2011 +0200
     9.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 20:20:36 2011 +0200
     9.3 @@ -179,8 +179,8 @@
     9.4        var nodes = previous.nodes
     9.5  
     9.6        edits foreach {
     9.7 -        case (name, Document.Node.Remove()) =>
     9.8 -          doc_edits += (name -> Document.Node.Remove())
     9.9 +        case (name, Document.Node.Clear()) =>
    9.10 +          doc_edits += (name -> Document.Node.Clear())
    9.11            nodes -= name
    9.12  
    9.13          case (name, Document.Node.Edits(text_edits)) =>
    10.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 16:07:26 2011 +0200
    10.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 20:20:36 2011 +0200
    10.3 @@ -210,8 +210,8 @@
    10.4            case None =>
    10.5              val (master_dir, path) = buffer_path(buffer)
    10.6              Thy_Header.thy_name(path) match {
    10.7 -              case Some(name) =>
    10.8 -                Some(Document_Model.init(session, buffer, master_dir, path, name))
    10.9 +              case Some((prefix, name)) =>
   10.10 +                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
   10.11                case None => None
   10.12              }
   10.13          }
   10.14 @@ -327,13 +327,17 @@
   10.15  
   10.16    private val file_store = new Session.File_Store
   10.17    {
   10.18 -    def append(master_dir: String, path: Path): String =
   10.19 +    def append(master_dir: String, source_path: Path): String =
   10.20      {
   10.21 -      val vfs = VFSManager.getVFSForPath(master_dir)
   10.22 -      if (vfs.isInstanceOf[FileVFS])
   10.23 -        MiscUtilities.resolveSymlinks(
   10.24 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   10.25 -      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   10.26 +      val path = source_path.expand
   10.27 +      if (path.is_absolute) Isabelle_System.platform_path(path)
   10.28 +      else {
   10.29 +        val vfs = VFSManager.getVFSForPath(master_dir)
   10.30 +        if (vfs.isInstanceOf[FileVFS])
   10.31 +          MiscUtilities.resolveSymlinks(
   10.32 +            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   10.33 +        else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   10.34 +      }
   10.35      }
   10.36  
   10.37      def require(canonical_name: String)