1 module Display where 2 3 import Core_datatype 4 5 import Edlib 6 7 import X_interface 8 9 import Kernel 10 11 import Parse 12 13 import Unparse 14 15 import Vtslib 16 17 import Type_defs 18 19 import Lookup 20 21 import Globals 22 23 import Tags 24 25 import Goals 26 27 import Tree 28 29 30 typeL = ["Thm","Trm","Sgn","Dec"] 31 32 33 wins = ["Own","Scratch"] 34 35 36 37 select :: (Eq b) => b -> [b] -> Int 38 39 select s [] = 0 40 41 select s (s' : l) = if s==s' then 0 else 1+select s l 42 43 44 45 make_form ty sp win err 46 = [ 47 InComment " Parse Object", 48 InRadio "Type of Object" 49 (case ty of 50 SOME x -> select x typeL 51 _ -> 0 ) 52 typeL , 53 InComment "", 54 InMultiText "Specification" 55 ( case sp of 56 SOME x -> x 57 _ -> "" ), 58 InRadio "Display Window" 59 ( case win of 60 SOME x -> select x wins 61 _ -> 0 ) 62 wins 63 ] ++ 64 (case err of 65 SOME err' -> [InComment err'] 66 _ -> []) 67 68 {- 69 unerr (Unbound s) = "Unbound symbol " ^ s 70 71 unerr (UnboundRec s) = "Unbound rec symbol " ^ s 72 73 unerr NonAtomic = "Not atomic" 74 75 unerr (NonInfixBinder s) = "Expected infixbinder, found " ^ s 76 77 unerr (NonNumber s) = "Not a number " ^ s 78 79 unerr (Reserved s) = "Unexpected reserved word " ^ s 80 81 unerr OtherError = "Syntax error" 82 -} 83 84 --eexperr t1 t2 = "Expected "^t1^" but found "^t2 85 86 87 theory_form = [ 88 InComment " Show Theory", 89 InRadio "Display Theory" 1 ["Strcutured","Unstructered", 90 "Just Names"] 91 ] 92 93 94 95 96 show_goal_cmd tr@(TreeSt t _ gst) 97 = x_display title display ./. 98 reTurn tr 99 where 100 title = (case obj of 101 ThmSpec _ -> "Thm Goal No: " 102 TrmSpec _ -> "Trm Goal No: " 103 SgnSpec _ -> "Sgn Goal No: " 104 DecSpec _ -> "Dec Goal No: " ) 105 ++ uid 106 display = unparse_obj sg gst obj 107 (Tree (Goal _ _ _ uid obj _ sg _) _ _ _ _ ) = t 108 109 110 111 show_subgoal_cmd :: Int -> (Tree_state GOAL b (c, d, e)) -> Xin 112 -> Xst ( MayBe (Tree_state GOAL b (c, d, e)) f ) 113 114 show_subgoal_cmd i tr@( TreeSt (Tree _ tl _ _ _) _ gst) 115 = x_display title display ./. 116 reTurn tr 117 where 118 title = ( case obj of 119 ThmSpec _ -> "Thm Goal No: " 120 TrmSpec _ -> "Trm Goal No: " 121 SgnSpec _ -> "Sgn Goal No: " 122 DecSpec _ -> "Dec Goal No: " ) 123 ++ uid 124 display = unparse_obj sg gst obj 125 ( Tree (Goal _ _ _ uid obj _ sg _) _ _ _ _ ) = tl !! i 126 127 128 129 show_theory tr@( TreeSt (Tree g _ _ _ _) _ gst) 130 = x_form True theory_form /./ 131 disp 132 where 133 disp ( SOME [(OutRadio "Strcutured")] ) 134 = show_theory' tr (unparse_Sgn (error "") (get_attributes gst)) g 135 disp ( SOME [(OutRadio "Unstructered")] ) 136 = show_theory' tr display_Sgn g 137 disp ( SOME [(OutRadio "Just Names")] ) 138 = show_theory' tr summary_Sgn g 139 disp _ = reTurn tr 140 141 display_Sgn = error "unimplemented in display" 142 summary_Sgn = error "unimplemented in display" 143 144 145 146 147 148 149 show_theory' tr unparse_fn (Goal _ _ _ uid _ True sg lt) 150 = x_display title display ./. 151 reTurn tr 152 where 153 title = "Signature of Node No. " ++ uid 154 display = unparse_fn sg 155 156 show_theory' tr unparse_fn (Goal _ _ _ _ _ False _ _) 157 = x_set_status "Theory not yet defined" ./. 158 reTurn tr 159 160 161 162 163 164 show_object tr@( TreeSt (Tree g _ _ _ _) _ gst) 165 = case g of 166 Goal _ _ _ uid _ True sg lt 167 -> show_obj sg gst' sg att NONE NONE NONE NONE /./ 168 ( \ _ -> reTurn tr ) 169 where 170 -- gst' = get_default_ps gst 171 gst' = gst -- find get_default_ps 172 att = get_attributes gst 173 Goal _ _ _ _ _ False _ _ 174 -> x_set_status "Theory not yet defined" ./. 175 reTurn tr 176 177 178 179 180 show_com t@(Tree (Goal _ _ (SOME com) uid _ _ _ _) _ _ _ _) 181 = x_display ("Comment for Node No: " ++ uid) com ./. 182 reTurn t 183 184 show_com t@(Tree (Goal _ _ NONE _ _ _ _ _) _ _ _ _) 185 = x_set_status "No Comment defined" ./. 186 reTurn t 187 188 189 get_comment (Tree (Goal _ _ NONE _ _ _ _ _) _ _ _ _) = "" 190 191 get_comment (Tree (Goal _ _ (SOME s) _ _ _ _ _) _ _ _ _) = s 192 193 194 195 196 set_comment "" (Tree (Goal a b _ d e f g h) i j k l) 197 = Tree (Goal a b NONE d e f g h) i j k l 198 199 set_comment c (Tree (Goal a b _ d e f g h) i j k l) 200 = Tree (Goal a b (SOME c) d e f g h) i j k l 201 202 203 204 205 unparse_obj sg gst (TrmSpec tm) 206 = unparse_trm sg (get_attributes gst) tm 207 208 unparse_obj sg gst (ThmSpec tm) 209 = unparse_trm sg (get_attributes gst) tm 210 211 unparse_obj sg gst (DecSpec dc) 212 = unparse_dec sg (get_attributes gst) dc 213 214 unparse_obj sg gst (SgnSpec isg) 215 = unparse_sgn sg (get_attributes gst) isg 216 217 218 219 {- no - valid result (Ok "" ) returned - only possibility of error - deal with this ? -} 220 221 show_obj sg ps lt attL ty sp win err 222 = x_form True (make_form ty sp win err) /./ 223 exp 224 where 225 exp NONE = reTurn "" 226 227 exp ( SOME [OutRadio obj_type, OutText obj_spec, OutRadio win] ) 228 = display_fn (show_fn obj_spec) ./. 229 reTurn "" 230 where 231 display_fn = case win of 232 "Own" -> own_win obj_type 233 "Scratch" -> scratch_win obj_type 234 _ -> own_win obj_type 235 show_fn = case obj_type of 236 "Trm" -> show_Trm sg ps lt attL 237 {- 238 "Thm" -> show_Thm sg ps lt attL 239 "Sgn" -> show_Sgn sg ps lt attL 240 "Dec" -> show_Dec sg ps lt attL 241 -} 242 _ -> show_error 243 244 -- exp _ = reTurn "" 245 246 {- 247 handle 248 Syntax (e,inp) => 249 let val err_mesg = unerr e 250 val where = under_line_input inp 251 val new_form = redo err_mesg where info 252 in show_obj xio sg ps lt attL new_form end 253 | Expect (t1,t2,inp) => 254 let val err_mesg = eexperr t1 t2 255 val where = under_line_input inp 256 val new_form = redo err_mesg where info 257 in show_obj xio sg ps lt attL new_form end 258 | Fail s => 259 let val err_mesg = "Error: "^ s 260 val where = "" 261 val new_form = redo err_mesg where info 262 in show_obj xio sg ps lt attL new_form end) 263 -} 264 265 266 267 268 {- 269 redo err whre (SOME [OutRadio obj_type, OutText obj_spec, OutRadio win]) 270 = [ 271 InComment "Parse Object", 272 InRadio "Type of Object" ["Trm","Thm","Sgn","Dec"], 273 InComment "Specification of Object", 274 InMultiText obj_spec, 275 InComment err, 276 InComment whre, 277 InRadio "Display Window" ["Own", "Scratch"] 278 ] 279 -} 280 281 282 283 284 285 show_Trm sg ps lt attL tm_rep 286 = unparse_Trm sg attL 287 (parse_tm (tgL,sg) tm_rep ) 288 -- (parse_typed_Trm tm_rep ps sg) 289 290 291 {- 292 show_Thm sg ps lt attL th_rep 293 = unparse_Thm lt attL 294 (parse_Thm th_rep ps sg) 295 296 297 298 show_Sgn sg ps lt attL sg_rep 299 = unparse_Sgn lt attL 300 (parse_typed_Sgn sg_rep ps) 301 302 303 304 show_Dec sg ps lt attL dc_rep 305 = unparse_Dec lt attL 306 (parse_typed_Dec dc_rep ps sg) 307 -} 308 309 310 show_error s = "Bad Object" 311 312 313 314 315 316 own_win = x_display 317 318 319 320 scratch_win obj_type s = x_scratch ("\n\n" ++ obj_type ++ "\n\n" ++ s) 321 322 323 324 split_line = split '\n' 325 326 327 328 329 show_comment tr@(TreeSt t _ _) 330 = show_com t /./ 331 (\ _ -> reTurn tr ) 332 333 334 335 edit_comment tr @ (TreeSt t tl gst) 336 = x_form True [InComment "Edit Comment", InMultiText "Comment:" com] /./ 337 exp 338 where 339 exp (SOME [OutText com']) 340 = reTurn ( TreeSt (set_comment com' t) tl gst ) 341 exp _ = reTurn tr 342 343 com = get_comment t 344 345 346 347 show_arguments tr@(TreeSt t _ _) 348 = show_args t ./. 349 reTurn tr 350 351 352 353 show_args t@(Tree (Goal (SOME tac) op_args _ uid _ _ _ _) _ _ _ _) 354 = x_display title concat_args 355 where 356 concat_args = case op_args of 357 NONE -> "NONE" 358 SOME args -> foldr ((++).(\s->s++ "\n\n")) "" args 359 title = "Node: " ++ uid ++ "\nTactic: " ++ tac ++ "\nArguments:" 360 361 show_args t@(Tree (Goal _ _ _ _ _ _ _ _) _ _ _ _) 362 = x_set_status "No tactic applied!" 363 364 365 show_tactics t = x_show_tactics ./. 366 reTurn t