1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Specify/test-out.sml	Sun May 10 17:26:36 2020 +0200
     1.3 @@ -0,0 +1,75 @@
     1.4 +(* Title: generate specific entries into Ctree
     1.5 +   Author: Walther Neuper
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +This will be dropped at switch to Isabelle/PIDE.
     1.9 +*)
    1.10 +
    1.11 +signature TEST_OUTPUT =
    1.12 +sig
    1.13 +  datatype pblmet = Method of Method.id | Problem of Problem.id | Upblmet
    1.14 +  datatype mout =
    1.15 +    EmptyMout
    1.16 +  | Error' of string
    1.17 +  | FormKF of TermC.as_string
    1.18 +  | PpcKF of pblmet * P_Model.item P_Model.ppc
    1.19 +  | RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
    1.20 +
    1.21 +  type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree
    1.22 +  val mout2str: mout -> string
    1.23 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.24 +  (* NONE *)
    1.25 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.26 +  (* NONE *)
    1.27 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.28 +end
    1.29 +
    1.30 +(**)     (*Generate*)
    1.31 +structure Test_Out(**): TEST_OUTPUT(**) =
    1.32 +struct
    1.33 +(**)
    1.34 +open Ctree
    1.35 +open Pos
    1.36 +
    1.37 +datatype pblmet =
    1.38 +  Upblmet
    1.39 +| Problem of Problem.id
    1.40 +| Method of Method.id;
    1.41 +fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)
    1.42 +  | pblmet2str (Method metID) = "Method " ^ Method.id_to_string metID (*%^%*)
    1.43 +  | pblmet2str x = error ("pblmet2str: uncovered definition " ^ pblmet2str x)
    1.44 +
    1.45 +(*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
    1.46 +datatype foppFK =                  (* in DG cases div 2 *)
    1.47 +  EmptyFoppFK         (*DG internal*)
    1.48 +| FormFK of TermC.as_string
    1.49 +| PpcFK of TermC.as_string P_Model.ppc
    1.50 +
    1.51 +datatype nest = Open | Closed | Nundef;
    1.52 +
    1.53 +type indent = int;
    1.54 +datatype edit = EdUndef | Write | Protect;
    1.55 +
    1.56 +datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
    1.57 +  Error_ of string                                                         (*<--*)
    1.58 +| FormKF of cellID * edit * indent * nest * TermC.as_string                   (*<--*)
    1.59 +| PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.item P_Model.ppc) (*<--*)
    1.60 +| RefineKF of Stool.match list                                             (*<--*)
    1.61 +| RefinedKF of (Problem.id * ((I_Model.T) * ((bool * term) list)))   (*<--*)
    1.62 +
    1.63 +datatype mout =
    1.64 +  FormKF of TermC.as_string
    1.65 +| PpcKF of (pblmet * P_Model.item P_Model.ppc) 
    1.66 +| RefinedKF of Problem.id * (I_Model.T * (bool * term) list)
    1.67 +| Error' of string
    1.68 +| EmptyMout
    1.69 +
    1.70 +fun mout2str (FormKF cterm') = "FormKF " ^ cterm'
    1.71 +  | mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ "," ^ P_Model.itemppc2str itemppc ^ ")"
    1.72 +  | mout2str (RefinedKF  (_, _)) = "mout2str: RefinedKF not impl."
    1.73 +  | mout2str (Error'  str) = "Error' " ^ str
    1.74 +  | mout2str (EmptyMout    ) = "EmptyMout"
    1.75 +
    1.76 +type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree;
    1.77 +
    1.78 +(**)end(**)
    1.79 \ No newline at end of file