<commit_before>(*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
    Author:     <NAME> and <NAME>

Isabelle/Isar configuration for Emacs Proof General.
See also http://proofgeneral.inf.ed.ac.uk
*)

signature PROOF_GENERAL =
sig
  val test_markupN: string
  val init: bool -> unit
  val init_outer_syntax: unit -> unit
  val sendback: string -> Pretty.T list -> unit
end;

structure ProofGeneral: PROOF_GENERAL =
struct


(* print modes *)

val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
val test_markupN = "test_markup";          (*XML markup for everything*)

fun special ch = Symbol.SOH ^ ch;


(* render markup *)

local

fun render_trees ts = fold render_tree ts
and render_tree (XML.Text s) = Buffer.add s
  | render_tree (XML.Elem (name, props, ts)) =
      let
        val (bg1, en1) =
          if name <> Markup.promptN andalso print_mode_active test_markupN
          then XML.output_markup (name, props)
          else Markup.no_output;
        val (bg2, en2) =
          if (case ts of [XML.Text _] => false | _ => true) then Markup.no_output
          else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
          else if name = Markup.sendbackN then (special "W", special "X")
          else if name = Markup.hiliteN then (special "0", special "1")
          else if name = Markup.tclassN then (special "B", special "A")
          else if name = Markup.tfreeN then (special "C", special "A")
          else if name = Markup.tvarN then (special "D", special "A")
          else if name = Markup.freeN then (special "E", special "A")
          else if name = Markup.boundN then (special "F", special "A")
          else if name = Markup.varN then (special "G", special "A")
          else if name = Markup.skolemN then (special "H", special "A")
          else Markup.no_output;<commit_msg>render_tree: suppress markup only for empty body (of status messages, cf. da275b7809bd) in order to recover hilite;<commit_after>(*  Title:      Pure/ProofGeneral/proof_general_emacs.ML
    Author:     <NAME> and <NAME>

Isabelle/Isar configuration for Emacs Proof General.
See also http://proofgeneral.inf.ed.ac.uk
*)

signature PROOF_GENERAL =
sig
  val test_markupN: string
  val init: bool -> unit
  val init_outer_syntax: unit -> unit
  val sendback: string -> Pretty.T list -> unit
end;

structure ProofGeneral: PROOF_GENERAL =
struct


(* print modes *)

val proof_generalN = "ProofGeneralEmacs";  (*token markup (colouring vars, etc.)*)
val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
val test_markupN = "test_markup";          (*XML markup for everything*)

fun special ch = Symbol.SOH ^ ch;


(* render markup *)

local

fun render_trees ts = fold render_tree ts
and render_tree (XML.Text s) = Buffer.add s
  | render_tree (XML.Elem (name, props, ts)) =
      let
        val (bg1, en1) =
          if name <> Markup.promptN andalso print_mode_active test_markupN
          then XML.output_markup (name, props)
          else Markup.no_output;
        val (bg2, en2) =
          if null ts then Markup.no_output
          else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
          else if name = Markup.sendbackN then (special "W", special "X")
          else if name = Markup.hiliteN then (special "0", special "1")
          else if name = Markup.tclassN then (special "B", special "A")
          else if name = Markup.tfreeN then (special "C", special "A")
          else if name = Markup.tvarN then (special "D", special "A")
          else if name = Markup.freeN then (special "E", special "A")
          else if name = Markup.boundN then (special "F", special "A")
          else if name = Markup.varN then (special "G", special "A")
          else if name = Markup.skolemN then (special "H", special "A")
          else Markup.no_output;
{'fraction_non_alphanumeric': 0.11293168641290648, 'fraction_numerical': 0.004789513486261659, 'mean_word_length': 2.764705882352941, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2392164', 'n_tokens_mistral': 1296, 'n_tokens_neox': 1266, 'n_words': 435}