(* Title: generate specific entries into Ctree

    Author: Walther Neuper

    (c) due to copyright terms

 This will be dropped at switch to Isabelle/PIDE .

 *)

 signature TEST_OUTPUT =

 sig

   datatype pblmet = MethodC of MethodC.id | Problem of Problem.id | Upblmet

   datatype mout =

     EmptyMout

   | Error' of string

   | FormKF of TermC.as_string

   | PpcKF of pblmet * P_Model.T

   | RefinedKF of Problem.id * (I_Model.T * Pre_Conds.T)

   type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree

   val mout2str: mout -> string

 end

 (**)     (*Generate*)

 structure Test_Out(**): TEST_OUTPUT(**) =

 struct

 (**)

 open Ctree

 open Pos

 datatype pblmet =

   Upblmet

 | Problem of Problem.id

 | MethodC of MethodC.id;

 fun pblmet2str (Problem pblID) = "Problem " ^ strs2str pblID (*%^%*)

   | pblmet2str (MethodC metID) = "MethodC " ^ MethodC.id_to_string metID (*%^%*)

   | pblmet2str x = raise ERROR ("pblmet2str: uncovered definition " ^ pblmet2str x)

 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)

 datatype foppFK =                  (* in DG cases div 2 *)

   EmptyFoppFK         (*DG internal*)

 | FormFK of TermC.as_string

 | PpcFK of TermC.as_string P_Model.model

 datatype nest = Open | Closed | Nundef;

 type indent = int;

 datatype edit = EdUndef | Write | Protect;

 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)

   Error_ of string                                                         (*<--*)

 | FormKF of cellID * edit * indent * nest * TermC.as_string                   (*<--*)

 | PpcKF of cellID * edit * indent * nest * (pblmet * P_Model.T) (*<--*)

 | RefineKF of M_Match.T list                                             (*<--*)

 | RefinedKF of (Problem.id * ((I_Model.T) * (Pre_Conds.T)))   (*<--*)

 datatype mout =

   FormKF of TermC.as_string

 | PpcKF of (pblmet * P_Model.T) 

 | RefinedKF of Problem.id * (I_Model.T * Pre_Conds.T)

 | Error' of string

 | EmptyMout

 fun mout2str (FormKF cterm') = "FormKF " ^ cterm'

   | mout2str (PpcKF  (pm, itemppc)) = "PpcKF (" ^ pblmet2str pm ^ ", " ^ P_Model.to_string itemppc ^ ")"

   | mout2str (RefinedKF  (_, _)) = "mout2str: RefinedKF not impl."

   | mout2str (Error'  str) = "Error' " ^ str

   | mout2str (EmptyMout    ) = "EmptyMout"

 type T = Pos.pos' * Pos.pos' list * mout * Ctree.ctree;

 (**)end(**)