New_node now takes a 'detached' argument.

src/ide/why3ide.ml

@@ -352,6 +352,7 @@ type pa_status = Controller_itp.proof_attempt_status
 let node_id_type : node_type Hint.t = Hint.create 17
 let node_id_proved : bool Hint.t = Hint.create 17
 let node_id_pa : pa_status Hint.t = Hint.create 17
+let node_id_detached : bool Hint.t = Hint.create 17
 
 let get_node_type id = Hint.find node_id_type id
 let get_node_proved id = Hint.find node_id_proved id
@@ -377,6 +378,9 @@ let node_id_to_gtree : GTree.row_reference Hint.t = Hint.create 42
 (* TODO exception for those: *)
 let get_node_row id = Hint.find node_id_to_gtree id
 
+let get_node_detached id =
+  Hint.find node_id_detached id
+
 (******************************)
 (* Initialization of the tree *)
 (******************************)
@@ -620,15 +624,19 @@ let image_of_pa_status ~obsolete pa =
 let set_status_column iter =
   let id = get_node_id iter in
   let proved = get_node_proved id in
+  let detached = get_node_detached id in
   let image = match get_node_type id with
     | NRoot -> assert false
     | NFile
     | NTheory
     | NTransformation
     | NGoal ->
-      if proved
-      then !image_valid
-      else !image_unknown
+      if detached then
+        !image_valid_obs
+      else
+        if proved
+        then !image_valid
+        else !image_unknown
     | NProofAttempt ->
       let pa = get_node_proof_attempt id in
       let obs = get_node_obs id in
@@ -636,10 +644,11 @@ let set_status_column iter =
   in
   goals_model#set ~row:iter ~column:status_column image
 
-let new_node ?parent ?(collapse=false) id name typ proved =
+let new_node ?parent ?(collapse=false) id name typ proved detached =
   if not (Hint.mem node_id_to_gtree id) then begin
     Hint.add node_id_type id typ;
     Hint.add node_id_proved id proved;
+    Hint.add node_id_detached id detached;
     let parent = Opt.map (fun x -> x#iter) parent in
     let iter = goals_model#append ?parent () in
     goals_model#set ~row:iter ~column:name_column name;
@@ -771,7 +780,11 @@ let on_selected_row r =
     let typ = get_node_type id in
     match typ with
     | NGoal ->
-      send_request (Get_task id)
+      let detached = get_node_detached id in
+      if detached then
+        task_view#source_buffer#set_text ""
+      else
+        send_request (Get_task id)
     | _ -> task_view#source_buffer#set_text ""
   with
     | Not_found -> task_view#source_buffer#set_text ""
@@ -960,12 +973,12 @@ let treat_notification n = match n with
           let iter = (get_node_row node)#iter in
           goals_view#selection#select_iter iter
     end
-  | New_node (id, parent_id, typ, name) ->
+  | New_node (id, parent_id, typ, name, detached) ->
     begin (try
         let parent = get_node_row parent_id in
-        ignore (new_node ~parent id name typ false)
+        ignore (new_node ~parent id name typ false detached)
       with Not_found ->
-        ignore (new_node id name typ false))
+        ignore (new_node id name typ false, detached))
     end
   | Remove id                     ->
     let n = get_node_row id in

src/ide/why3web.ml

@@ -62,9 +62,9 @@ let notification n =
   match n with
   | Node_change(nid,_info) ->
      Obj ["notification",String "Node_change"; "nid", Int nid; "info",String "TODO"]
-  | New_node(nid,parent,nt,name) ->
+  | New_node(nid,parent,nt,name,detached) ->
      Obj ["notification",String "New_node"; "nid", Int nid; "parent", Int parent;
-          "nodetype", String (nodetype nt); "name",String name]
+          "nodetype", String (nodetype nt); "name",String name; "detached",Bool detached]
   | Remove nid ->
      Obj ["notification",String "Remove"; "nid", Int nid]
   | Initialized _ginfo ->

src/session/itp_server.ml

@@ -311,9 +311,9 @@ type update_info =
       * Call_provers.resource_limit
 
 type notification =
-  | New_node     of node_ID * node_ID * node_type * string
+  | New_node     of node_ID * node_ID * node_type * string * bool
   (* Notification of creation of new_node:
-     New_node (new_node, parent_node, node_type, name). *)
+     New_node (new_node, parent_node, node_type, name, detached). *)
   | Node_change  of node_ID * update_info
   (* inform that the data of the given node changed *)
   | Remove       of node_ID
@@ -383,15 +383,15 @@ let print_msg fmt m =
 
 let print_notify fmt n =
   match n with
-  | Node_change (_ni, _nf)          -> fprintf fmt "node change"
-  | New_node (ni, _pni, _nt,  _nf)  -> fprintf fmt "new node %d" ni
-  | Remove _ni                      -> fprintf fmt "remove"
-  | Initialized _gi                 -> fprintf fmt "initialized"
-  | Saved                           -> fprintf fmt "saved"
-  | Message msg                     ->
+  | Node_change (_ni, _nf)             -> fprintf fmt "node change"
+  | New_node (ni, _pni, _nt,  _nf, _d) -> fprintf fmt "new node %d" ni
+  | Remove _ni                         -> fprintf fmt "remove"
+  | Initialized _gi                    -> fprintf fmt "initialized"
+  | Saved                              -> fprintf fmt "saved"
+  | Message msg                        ->
       print_msg fmt msg
-  | Dead s                          -> fprintf fmt "dead :%s" s
-  | Task (_ni, _s)                  -> fprintf fmt "task"
+  | Dead s                             -> fprintf fmt "dead :%s" s
+  | Task (_ni, _s)                     -> fprintf fmt "task"
 
 module type Protocol = sig
   val get_requests : unit -> ide_request list
@@ -529,6 +529,10 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
       let pa = get_proof_attempt_node d.cont.controller_session pa in
       Pp.string_of Whyconf.print_prover pa.prover
 
+  let get_node_detached (node: any) =
+    let d = get_server_data () in
+    is_detached d.cont.controller_session node
+
 (*
   let get_node_proved (node: any) =
     match node with
@@ -623,8 +627,9 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
       Hint.add model_any new_id node;
       let node_type = get_node_type node in
       let node_name = get_node_name node in
+      let node_detached = get_node_detached node in
       add_node_to_table node new_id;
-      P.notify (New_node (new_id, parent, node_type, node_name));
+      P.notify (New_node (new_id, parent, node_type, node_name, node_detached));
       new_id
 
   let root = 0
@@ -703,7 +708,7 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
       root f
 
   let init_and_send_the_tree (): unit =
-    P.notify (New_node (0, 0, NRoot, "root"));
+    P.notify (New_node (0, 0, NRoot, "root", false));
     iter_the_files (fun ~parent id -> ignore (new_node ~parent id)) root
 
   let resend_the_tree (): unit =
@@ -711,8 +716,9 @@ module Make (S:Controller_itp.Scheduler) (P:Protocol) = struct
       let node_id = node_ID_from_any any in
       let node_name = get_node_name any in
       let node_type = get_node_type any in
-      P.notify (New_node (node_id, parent, node_type, node_name)) in
-    P.notify (New_node (0, 0, NRoot, "root"));
+      let node_detached = get_node_detached any in
+      P.notify (New_node (node_id, parent, node_type, node_name, node_detached)) in
+    P.notify (New_node (0, 0, NRoot, "root", false));
     iter_the_files send_node root
 
   (* -- send the task -- *)

src/session/itp_server.mli

@@ -58,9 +58,9 @@ type update_info =
       * Call_provers.resource_limit
 
 type notification =
-  | New_node     of node_ID * node_ID * node_type * string
+  | New_node     of node_ID * node_ID * node_type * string * bool
   (* Notification of creation of new_node:
-     New_node (new_node, parent_node, node_type, name). *)
+     New_node (new_node, parent_node, node_type, name, detached). *)
   | Node_change  of node_ID * update_info
   (* inform that the data of the given node changed *)
   | Remove       of node_ID

src/session/json_util.ml

@@ -245,12 +245,13 @@ let convert_message (m: message_notification) =
 let print_notification_to_json (n: notification): json_object =
   let cc = convert_notification_constructor in
   match n with
-  | New_node (nid, parent, node_type, name) ->
+  | New_node (nid, parent, node_type, name, detached) ->
       Assoc ["notification", cc n;
              "node_ID", Int nid;
              "parent_ID", Int parent;
              "node_type", convert_node_type node_type;
-             "name", String name]
+             "name", String name;
+             "detached", Bool detached]
   | Node_change (nid, update) ->
       Assoc ["notification", cc n;
              "node_ID", Int nid;
@@ -528,8 +529,9 @@ let parse_notification constr l =
   | "New_node", ["node_ID", Int nid;
                  "parent_ID", Int parent;
                  "node_type", node_type;
-                 "name", String name] ->
-      New_node (nid, parent, parse_node_type_from_json node_type, name)
+                 "name", String name;
+                 "detached", Bool detached] ->
+      New_node (nid, parent, parse_node_type_from_json node_type, name, detached)
   | "Node_change", ["node_ID", Int nid;
                     "update", update] ->
       Node_change (nid, parse_update update)

src/session/session_itp.ml

@@ -98,7 +98,7 @@ let dummy_session =
    session_dir           = "";
    session_files         = Hstr.create 23;
    session_shape_version = 0;
-   session_prover_ids    = Hprover.create 23
+   session_prover_ids    = Hprover.create 23;
  }
 
 let theory_parent s th =
@@ -250,6 +250,29 @@ let get_proof_parent (s : session) (id : proofNodeID) =
 let get_trans_parent (s : session) (id : transID) =
   (get_transfNode s id).transf_parent
 
+(* TODO to be done with detached transformations *)
+let get_detached_trans (_s: session) (_id: proofNodeID) =
+  []
+
+let is_detached (s: session) (a: any) =
+  match a with
+  | AFile _file -> false
+  | ATh th     ->
+    let parent_name = th.theory_parent_name in
+    let parent = Hstr.find s.session_files parent_name in
+    List.exists (fun x -> x = th) parent.file_detached_theories
+  | ATn tn     ->
+    let pn_id = get_trans_parent s tn in
+    let pn = get_proofNode s pn_id in
+    pn.proofn_task = None || List.exists (fun x -> x = tn) (get_detached_trans s pn_id)
+  | APn pn     ->
+    let pn = get_proofNode s pn in
+    pn.proofn_task = None
+  | APa pa     ->
+    let pa = get_proof_attempt_node s pa in
+    let pn_id = pa.parent in
+    let pn = get_proofNode s pn_id in
+    pa.proof_obsolete || pn.proofn_task = None
 
 (* Remove elements of the session tree *)
 

src/session/session_itp.mli

@@ -92,8 +92,12 @@ val get_proof_name : session -> proofNodeID -> Ident.ident
 val get_proof_parent : session -> proofNodeID -> proof_parent
 val get_trans_parent : session -> transID -> proofNodeID
 
+val get_detached_trans : session -> proofNodeID -> transID list
 val get_any_parent: session -> any -> any option
 
+(* Answers true if a node is in a detached subtree *)
+val is_detached: session -> any -> bool
+
 exception BadCopyDetached
 
 (** [copy s pn] copy pn and add the copy as detached subgoal of its parent *)

src/why3shell/why3shell.ml

@@ -130,7 +130,8 @@ type node = {
   node_trans_args: string list option;
   node_type: shell_node_type;
   mutable node_proved: bool;
-  mutable children_nodes: node_ID list
+  mutable children_nodes: node_ID list;
+  mutable node_detached: bool
   }
 
 let root_node_ID = root_node
@@ -145,7 +146,8 @@ let root_node = {
   node_trans_args = None;
   node_type = SRoot;
   node_proved = false;
-  children_nodes = []
+  children_nodes = [];
+  node_detached = false
 }
 
 open Stdlib
@@ -179,7 +181,7 @@ let return_proof_info (t: node_type) =
     Some Controller_itp.Scheduled
   | _ -> None
 
-let add_new_node fmt (n: node_ID) (parent: node_ID) (t: node_type) (name: string) =
+let add_new_node fmt (n: node_ID) (parent: node_ID) (t: node_type) (name: string) (detached: bool) =
   if t = NRoot then () else
   let new_node = {
     node_ID = n;
@@ -190,7 +192,8 @@ let add_new_node fmt (n: node_ID) (parent: node_ID) (t: node_type) (name: string
     node_trans_args = None; (* TODO *)
     node_type = convert_to_shell_type t;
     node_proved = false;
-    children_nodes = []
+    children_nodes = [];
+    node_detached = detached
   } in
   try
     let parent = Hnode.find nodes parent in
@@ -222,8 +225,8 @@ let treat_notification fmt n =
   match n with
   | Node_change (id, info)        ->
     change_node fmt id info
-  | New_node (id, pid, typ, name) ->
-    add_new_node fmt id pid typ name
+  | New_node (id, pid, typ, name, detached) ->
+    add_new_node fmt id pid typ name detached
   | Remove _id                    -> (* TODO *)
     fprintf fmt "got a Remove notification not yet supported@."
   | Initialized _g_info           ->