Merge pull request #1319 from GaloisInc/T1313

Make `:module` work more like `:load`.
GaloisInc · Feb 8, 2022 · 335216f · 335216f
2 parents 413788c + 2d1f2c1
commit 335216f
Show file tree

Hide file tree

Showing 7 changed files with 18 additions and 9 deletions.
diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs
@@ -1124,9 +1124,18 @@ moduleCmd :: String -> REPL ()
 moduleCmd modString
   | null modString = return ()
   | otherwise      = do
-      case parseModName modString of
-        Just m  -> loadHelper (M.loadModuleByName m)
-        Nothing -> rPutStrLn "Invalid module name."
+    case parseModName modString of
+      Just m
+        | M.isParamInstModName m -> loadHelper (M.loadModuleByName m)
+        | otherwise  ->
+          do mpath <- liftModuleCmd (M.findModule m)
+             case mpath of
+               M.InFile file ->
+                 do setEditPath file
+                    setLoadedMod LoadedModule { lName = Just m, lPath = mpath }
+                    loadHelper (M.loadModuleByPath file)
+               M.InMem {} -> loadHelper (M.loadModuleByName m)
+      Nothing -> rPutStrLn "Invalid module name."
 
 loadPrelude :: REPL ()
 loadPrelude  = moduleCmd $ show $ pp M.preludeName

diff --git a/tests/modsys/T14.icry.stdout b/tests/modsys/T14.icry.stdout
@@ -1,4 +1,4 @@
 Loading module Cryptol
 
-Parse error at ./T14/Main.cry:3:9,
+Parse error at T14/Main.cry:3:9,
   unexpected: MalformedUtf8
diff --git a/tests/modsys/T14.icry.stdout.mingw32 b/tests/modsys/T14.icry.stdout.mingw32
@@ -1,4 +1,4 @@
 Loading module Cryptol
 
-Parse error at .\T14\Main.cry:3:9,
+Parse error at T14\Main.cry:3:9,
   unexpected: MalformedUtf8
diff --git a/tests/modsys/T16.icry.stdout b/tests/modsys/T16.icry.stdout
@@ -3,7 +3,7 @@ Loading module Cryptol
 Loading module T16::A
 Loading module T16::B
 
-[error] at ./T16/B.cry:5:5--5:11
+[error] at T16/B.cry:5:5--5:11
     Multiple definitions for symbol: update
     (at Cryptol:899:11--899:17, update)
     (at ./T16/A.cry:3:1--3:7, T16::A::update)
diff --git a/tests/modsys/T16.icry.stdout.mingw32 b/tests/modsys/T16.icry.stdout.mingw32
@@ -3,7 +3,7 @@ Loading module Cryptol
 Loading module T16::A
 Loading module T16::B
 
-[error] at .\T16\B.cry:5:5--5:11
+[error] at T16\B.cry:5:5--5:11
     Multiple definitions for symbol: update
     (at Cryptol:899:11--899:17, update)
     (at .\T16\A.cry:3:1--3:7, T16::A::update)
diff --git a/tests/modsys/T18.icry.stdout b/tests/modsys/T18.icry.stdout
@@ -4,7 +4,7 @@ Loading module T18::A
 Loading module T18::A1
 Loading module T18::B
 
-[error] at ./T18/B.cry:6:5--6:6
+[error] at T18/B.cry:6:5--6:6
     Multiple definitions for symbol: u
     (at ./T18/A.cry:3:1--3:2, T18::A::u)
     (at ./T18/A1.cry:3:1--3:2, T18::A1::u)
diff --git a/tests/modsys/T18.icry.stdout.mingw32 b/tests/modsys/T18.icry.stdout.mingw32
@@ -4,7 +4,7 @@ Loading module T18::A
 Loading module T18::A1
 Loading module T18::B
 
-[error] at .\T18\B.cry:6:5--6:6
+[error] at T18\B.cry:6:5--6:6
     Multiple definitions for symbol: u
     (at .\T18\A.cry:3:1--3:2, T18::A::u)
     (at .\T18\A1.cry:3:1--3:2, T18::A1::u)