summaryrefslogtreecommitdiff
path: root/src/exper/EditShell.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/exper/EditShell.hs')
-rw-r--r--src/exper/EditShell.hs6
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"