1 (* Title: generate specific entries into Ctree
3 (c) due to copyright terms
5 This will be dropped at switch to Isabelle/PIDE.
8 signature TEST_OUTPUT =
10 datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
14 | FormKF of TermC.as_string
15 | PpcKF of pblmet * P_Model.item P_Model.ppc
16 | RefinedKF of Problem.id * (I_Model.T * Pre_Conds.T)
18 type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree
19 val mout2str: mout -> string
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
28 structure Test_Out(**): TEST_OUTPUT(**) =
36 | Problem of Problem.id
37 | Method of Method.id;
38 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
39 | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)
40 | pblmet2str x = raise ERROR ("pblmet2str: uncovered definition " ^ pblmet2str x)
42 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
43 datatype foppFK = (* in DG cases div 2 *)
44 EmptyFoppFK (*DG internal*)
45 | FormFK of TermC.as_string
46 | PpcFK of TermC.as_string P_Model.ppc
48 datatype nest = Open | Closed | Nundef;
51 datatype edit = EdUndef | Write | Protect;
53 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
54 Error_ of string (*<--*)
55 | FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*)
56 | PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.item P_Model.ppc) (*<--*)
57 | RefineKF of Stool.match list (*<--*)
58 | RefinedKF of (Problem.id * ((I_Model.T) * (Pre_Conds.T))) (*<--*)
61 FormKF of TermC.as_string
62 | PpcKF of (pblmet * P_Model.item P_Model.ppc)
63 | RefinedKF of Problem.id * (I_Model.T * Pre_Conds.T)
67 fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
68 | mout2str (PpcKF (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ P_Model.itemppc2str itemppc ^ ")"
69 | mout2str (RefinedKF (_, _)) = "mout2str: RefinedKF not impl."
70 | mout2str (Error' str) = "Error' " ^ str
71 | mout2str (EmptyMout ) = "EmptyMout"
73 type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree;