equal
deleted
inserted
replaced
342 fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt; |
342 fun read_props ctxt = map (parse_prop ctxt) #> check_props ctxt; |
343 |
343 |
344 val read_term = singleton o read_terms; |
344 val read_term = singleton o read_terms; |
345 val read_prop = singleton o read_props; |
345 val read_prop = singleton o read_props; |
346 |
346 |
347 val read_sort_global = read_sort o ProofContext.init_global; |
347 val read_sort_global = read_sort o Proof_Context.init_global; |
348 val read_typ_global = read_typ o ProofContext.init_global; |
348 val read_typ_global = read_typ o Proof_Context.init_global; |
349 val read_term_global = read_term o ProofContext.init_global; |
349 val read_term_global = read_term o Proof_Context.init_global; |
350 val read_prop_global = read_prop o ProofContext.init_global; |
350 val read_prop_global = read_prop o Proof_Context.init_global; |
351 |
351 |
352 |
352 |
353 (* pretty = uncheck + unparse *) |
353 (* pretty = uncheck + unparse *) |
354 |
354 |
355 fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt; |
355 fun pretty_term ctxt = singleton (uncheck_terms ctxt) #> unparse_term ctxt; |
368 (* global pretty printing *) |
368 (* global pretty printing *) |
369 |
369 |
370 val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false))); |
370 val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false))); |
371 fun is_pretty_global ctxt = Config.get ctxt pretty_global; |
371 fun is_pretty_global ctxt = Config.get ctxt pretty_global; |
372 val set_pretty_global = Config.put pretty_global; |
372 val set_pretty_global = Config.put pretty_global; |
373 val init_pretty_global = set_pretty_global true o ProofContext.init_global; |
373 val init_pretty_global = set_pretty_global true o Proof_Context.init_global; |
374 |
374 |
375 val pretty_term_global = pretty_term o init_pretty_global; |
375 val pretty_term_global = pretty_term o init_pretty_global; |
376 val pretty_typ_global = pretty_typ o init_pretty_global; |
376 val pretty_typ_global = pretty_typ o init_pretty_global; |
377 val pretty_sort_global = pretty_sort o init_pretty_global; |
377 val pretty_sort_global = pretty_sort o init_pretty_global; |
378 |
378 |