From db65b6bce10b16423eb30cc986aee39e7d08fb56 Mon Sep 17 00:00:00 2001 From: aarne Date: Wed, 10 Dec 2008 14:20:52 +0000 Subject: added and editor function allMetas showing all meta positions and their types --- src/exper/EditShell.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src/exper') 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" -- cgit v1.2.3