equal
deleted
inserted
replaced
966 |
966 |
967 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE |
967 fun gpt_cell (Nd (PblObj {cell = c,...},_)) = NONE |
968 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c; |
968 | gpt_cell (Nd (PrfObj {cell = c,...},_)) = c; |
969 |
969 |
970 (* get the formula preceeding the current position in a calculation *) |
970 (* get the formula preceeding the current position in a calculation *) |
971 fun get_pred_formula (pt, pos as (p, p_)) = |
971 fun get_curr_formula (pt, pos as (p, p_)) = |
972 case p_ of |
972 case p_ of |
973 Frm => get_obj g_form pt p |
973 Frm => get_obj g_form pt p |
974 | Res => (fst o (get_obj g_result pt)) p |
974 | Res => (fst o (get_obj g_result pt)) p |
975 | _ => #3 (get_obj g_origin pt p); |
975 | _ => #3 (get_obj g_origin pt p); |
976 |
976 |