Use search path when parsing a document.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>

src/params.ml

@@ -271,6 +271,10 @@ let add_search_dir dir =
   if List.for_all (fun lp -> lp <> dir) !rev_search_path then
     rev_search_path := library_path :: dir :: List.tl !rev_search_path
 
+(* Reset the search path to the specified list. *)
+let set_search_path dirs =
+  rev_search_path := library_path :: List.concat [dirs; Setup_paths.Sites.stdlib]
+
 let output_dir = ref "."
 
 let default_method =

src/params.mli

@@ -87,6 +87,7 @@ val fpf_in: string option ref
 val summary: bool ref
 val stats: bool ref
 val add_search_dir: string -> unit
+val set_search_path: string list -> unit
 val keep_going: bool ref  (* FIXME check still used ? *)
 val suppress_all: bool ref
 val set_smt_logic: string -> unit

src/tlapm_lib.ml

@@ -609,17 +609,18 @@ let module_of_string (content : string) (fn : string) : (Module.T.mule, (string
         let hint = Property.assign hint Module.Save.module_content_prop (Module.Save.String content) in
         let mule = Module.Save.parse_file ~clock:Clocks.parsing hint in
         Params.input_files := [Filename.basename fn]; (* Needed, because p_gen.ml decides if obs should be generated by this. *)
+        Params.set_search_path [Filename.dirname fn]; (* Were to look for referenced files. TODO: Take additional. *)
         mule.core.important <- true ;
         let mcx = Module.Standard.initctx in
         let mcx = Sm.add mule.core.name.core mule mcx in
         let mcx = Module.Save.complete_load ~clock:Clocks.parsing mcx in
         let (mcx, mods) = Module.Dep.schedule mcx in
-        match List.filter (fun m -> m.core.important) mods with
+        match List.filter (fun m -> m.core.name.core = mule.core.name.core) mods with
         | [mule] ->
             let (_mcx, mule, _summ) = Module.Elab.normalize mcx Deque.empty mule in
             Ok mule
-        | [] -> failwith "module_of_string, no important mules"
-        | _ -> failwith "module_of_string, too many important mules"
+        | [] -> failwith "module_of_string, found no module we tried to parse."
+        | _ -> failwith "module_of_string, found too many modules with required name."
     in
     match parse_it () with
     | Ok mule -> Ok mule