src/Pure/Isar/proof_context.ML
changeset 39045 30f3d9daaa3a
parent 38980 af73cf0dc31f
child 39136 b0b3b6318e3b
equal deleted inserted replaced
39044:5c13736e81c7 39045:30f3d9daaa3a
   739 
   739 
   740 fun parse_sort ctxt text =
   740 fun parse_sort ctxt text =
   741   let
   741   let
   742     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
   742     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
   743     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
   743     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
   744       handle ERROR msg => cat_error msg ("Failed to parse sort" ^ Position.str_of pos)
   744       handle ERROR msg => cat_error msg "Failed to parse sort";
   745   in Type.minimize_sort (tsig_of ctxt) S end;
   745   in Type.minimize_sort (tsig_of ctxt) S end;
   746 
   746 
   747 fun parse_typ ctxt text =
   747 fun parse_typ ctxt text =
   748   let
   748   let
   749     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
   749     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
   750     val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
   750     val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
   751       handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
   751       handle ERROR msg => cat_error msg "Failed to parse type";
   752   in T end;
   752   in T end;
   753 
   753 
   754 fun parse_term T ctxt text =
   754 fun parse_term T ctxt text =
   755   let
   755   let
   756     val {get_sort, map_const, map_free} = term_context ctxt;
   756     val {get_sort, map_const, map_free} = term_context ctxt;
   757 
   757 
   758     val (T', _) = Type_Infer.paramify_dummies T 0;
   758     val (T', _) = Type_Infer.paramify_dummies T 0;
   759     val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
   759     val (markup, kind) =
       
   760       if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
   760     val (syms, pos) = Syntax.parse_token ctxt markup text;
   761     val (syms, pos) = Syntax.parse_token ctxt markup text;
   761 
   762 
   762     fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
   763     fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
   763       handle ERROR msg => SOME msg;
   764       handle ERROR msg => SOME msg;
   764     val t =
   765     val t =
   765       Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
   766       Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
   766         ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
   767         ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
   767       handle ERROR msg => cat_error msg ("Failed to parse " ^ kind ^ Position.str_of pos);
   768       handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
   768   in t end;
   769   in t end;
   769 
   770 
   770 
   771 
   771 fun unparse_sort ctxt =
   772 fun unparse_sort ctxt =
   772   Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}
   773   Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}