diff options
Diffstat (limited to 'src/exper')
| -rw-r--r-- | src/exper/EditShell.hs | 6 |
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" |
