1.1 --- a/src/Tools/isac/ProgLang/termC.sml	Sat Feb 18 15:00:54 2017 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/termC.sml	Wed May 31 14:58:38 2017 +0200
     1.3 @@ -20,6 +20,38 @@
     1.4      (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
     1.5      handle _ => false
     1.6  
     1.7 +(**
     1.8 +  transform  typ / term to a String, which is parsed by Scala
     1.9 +  after transport via libisabelle
    1.10 +*)
    1.11 +fun scala_of_typ (Type (s, typs)) =
    1.12 +    enclose "Type(" ")" (quote s ^ ", " ^
    1.13 +      (typs |> map scala_of_typ |> commas |> enclose "List(" ")"))
    1.14 +  | scala_of_typ (TFree (s, sort)) =
    1.15 +    enclose "TFree(" ")" (quote s ^ ", " ^ (sort |> map quote |> commas |> enclose "List(" ")"))
    1.16 +  | scala_of_typ (TVar ((s, i), sort)) =
    1.17 +    enclose "TVar(" ")" (
    1.18 +      enclose "(" ")," (quote s ^ "," ^ quote (string_of_int i)) ^ 
    1.19 +      (sort |> map quote |> commas |> enclose "List(" ")"))
    1.20 +
    1.21 +fun scala_of_term (Const (s, T)) =
    1.22 +    enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T)
    1.23 +  | scala_of_term (Free (s, T)) =
    1.24 +    enclose "Free(" ")" (quote s ^ ", " ^ scala_of_typ T)
    1.25 +  | scala_of_term (Var ((s, i), T)) =
    1.26 +    enclose "TVar(" ")" (
    1.27 +      enclose "(" ")," (quote s ^ "," ^ quote (string_of_int i)) ^ 
    1.28 +      scala_of_typ T)
    1.29 +  | scala_of_term (Bound i) = enclose "Bound(" ")" (string_of_int i)
    1.30 +  | scala_of_term (Abs (s, T, t)) =
    1.31 +    enclose "Abs(" ")" (
    1.32 +      quote s ^ ", " ^
    1.33 +      scala_of_typ T ^ ", " ^
    1.34 +      scala_of_term t)
    1.35 +  | scala_of_term (t1 $ t2) =
    1.36 +    enclose "App(" ")" (scala_of_term t1 ^ ", " ^ scala_of_term t2)
    1.37 +
    1.38 +(** old versions *)
    1.39  fun atomtyp t = (*WN10 see raw_pp_typ*)
    1.40    let
    1.41      fun ato n (Type (s,[])) = 

     2.1 --- a/test/Tools/isac/Test_Isac.thy	Sat Feb 18 15:00:54 2017 +0100
     2.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed May 31 14:58:38 2017 +0200
     2.3 @@ -68,7 +68,8 @@
     2.4  
     2.5  ML {*
     2.6  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     2.7 -                      (* these vvv test, if funs are intermediately opened in structure *)
     2.8 +                      (* these vvv test, if funs are intermediately opened in structure 
     2.9 +                         in case of errors here consider ~~/./xtest-to-coding.sh      *)
    2.10    open Kernel;
    2.11    open Math_Engine;            CalcTreeTEST;
    2.12    open Lucin;                  appy;