src/Pure/proof_general.ML

 
 local
 
 val spaces_quote = space_implode " " o map quote;
 
-(* FIXME: investigate why dependencies at the moment include themselves! *)
 fun thm_deps_message (thms, deps) =
   if pgip() then
     issue_pgips
       [XML.element
         "metainforesponse"  (* FIXME: get thy name from info here? *)
         [("infotype", "isabelle_theorem_dependencies")]
         [XML.element "value" [("name", "thms")] [XML.text thms],
          XML.element "value" [("name", "deps")] [XML.text deps]]]
   else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
 
+(* FIXME: check this uses non-transitive closure function here *)
 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   let
     val names = filter_out (equal "") (map Thm.name_of_thm ths);
     val deps = filter_out (equal "")
       (Symtab.keys (fold Proofterm.thms_of_proof

   val thyname_attro = xmlattro "thyname"
   val thyname_attr = xmlattr "thyname"
   val objtype_attro = xmlattro "objtype"
   val objtype_attr = xmlattr "objtype"
   val name_attr = xmlattr "name"
-  val dirname_attr = xmlattr "dir"
-  fun comment x = "(* " ^ x ^ " *)"
 
   fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
       case Url.unpack url of
           (Url.File path) => File.platform_path path
         | _ => error ("Cannot access non-local URL " ^ url)

   val currently_open_file = ref (NONE : string option)
 
   (* Path management: we allow theory files to have dependencies
      in their own directory, but when we change directory for a new
      file we remove the path.  Leaving it there can cause confusion
-     with difference in batch mode.a  NB: PGIP does not assume
+     with difference in batch mode. NB: PGIP does not currently assume
      that the prover has a load path. *)
   local
       val current_working_dir = ref (NONE : string option)
   in
       fun changecwd dir =