1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml	Fri Sep 16 12:13:23 2022 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml	Mon Sep 26 10:57:53 2022 +0200
     1.3 @@ -74,9 +74,11 @@
     1.4    val parseNEW: Proof.context -> string -> term option
     1.5    val parseNEW': Proof.context -> string -> term
     1.6    val parseNEW'': theory -> string -> term
     1.7 -  val parse_strict: theory -> string -> term
     1.8 +  val parse_strict: theory -> string -> term (*still required for CAS_Cmd*)
     1.9 +  val parse_strict_PIDE: theory -> string -> term
    1.10  
    1.11    val parse_patt: theory -> string -> term
    1.12 +  val parse_patt_PIDE: theory -> string -> term
    1.13    val perm: term -> term -> bool
    1.14  
    1.15    val str_of_free_opt: term -> string option
    1.16 @@ -535,6 +537,7 @@
    1.17    | T_a2real (TVar (("DUMMY", _), _)) = HOLogic.realT
    1.18    | T_a2real (TVar ((s, i), srt)) = 
    1.19      if s = "'a" orelse s = "'b" orelse s = "'c" then HOLogic.realT else TVar ((s, i), srt)
    1.20 +(*val typ_a2real: term -> term*)
    1.21  fun typ_a2real (Const( s, T)) = (Const( s, T_a2real T)) 
    1.22    | typ_a2real (Free( s, T)) = (Free( s, T_a2real T))
    1.23    | typ_a2real (Var( n, T)) = (Var( n, T_a2real T))
    1.24 @@ -553,8 +556,8 @@
    1.25      SOME t => t
    1.26    | NONE => raise TERM ("NO parseNEW'' for " ^ str, [])
    1.27  
    1.28 -(* TODO clarify parse with Test_Isac *)
    1.29 -fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str);
    1.30 +fun parse_strict thy str = typ_a2real (Syntax.read_term_global thy str); (*still required for CAS_Cmd*)
    1.31 +fun parse_strict_PIDE thy str = (*typ_a2real*) (Syntax.read_term_global thy str);
    1.32  
    1.33  (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
    1.34    WN130613 probably compare to 
    1.35 @@ -564,6 +567,11 @@
    1.36    |-> Proof_Context.read_term_pattern
    1.37  (*|> numbers_to_string   TODO drop*)
    1.38    |> typ_a2real;       (*TODO drop*)
    1.39 +fun parse_patt_PIDE thy str = (thy, str)
    1.40 +  |>> Proof_Context.init_global
    1.41 +  |-> Proof_Context.read_term_pattern
    1.42 +(*|> numbers_to_string   TODO drop*)
    1.43 +(*|> typ_a2real;         TODO drop*)
    1.44  fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
    1.45  
    1.46  fun is_atom (Const _) = true