added and editor function allMetas showing all meta positions and their types

1 files changed, 5 insertions, 1 deletions

diff --git a/src/exper/EditShell.hs b/src/exper/EditShell.hs
index 40a8741e3..e5923ef18 100644
--- a/src/exper/EditShell.hs
+++ b/src/exper/EditShell.hs
@@ -66,6 +66,9 @@ interpret pgf dict st c = case words c of
     let st' = goNext st
     prLState pgf st'
     return st'
+  "x":_ -> do
+    mapM_ putStrLn [show (showPosition p) ++ showType t  | (p,t) <- allMetas st]
+    return st
   "h":_ -> putStrLn commandHelp >> return st
   _ -> do
     putStrLn "command not understood"
@@ -96,7 +99,8 @@ commandHelp = unlines [
   "h           -- display this help message",
   "m           -- show refinement menu",
   "p Anything  -- parse Anything and refine with it",
-  "r Function  -- refine with Function", 
+  "r Function  -- refine with Function",
+  "x           -- show all unknown positions and their types", 
   "4           -- refine with 4th item from menu (see m)", 
   "[1,2,3]     -- go to position 1,2,3",
   ">           -- go to next node"