<commit_before>(*  Title:      Pure/Tools/proof_general.ML
    Author:     <NAME>
    Author:     Makarius

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

signature PROOF_GENERAL =
sig
  type category = string
  val category_display: category
  val category_advanced_display: category
  val category_tracing: category
  val category_proof: category
  type pgiptype = string
  val pgipbool: pgiptype
  val pgipint: pgiptype
  val pgipfloat: pgiptype
  val pgipstring: pgiptype
  val preference_raw: category ->
    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
  val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
  val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
  val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
  val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
  val preference_option: category -> string -> string -> string -> unit
  structure ThyLoad: sig val add_path: string -> unit end
  val thm_deps: bool Unsynchronized.ref
  val proof_generalN: string
  val init: unit -> unit
end;

structure ProofGeneral: PROOF_GENERAL =
struct

(** preferences **)

(* type preference *)

type category = string;
val category_display = "Display";
val category_advanced_display = "Advanced Display";
val category_tracing = "Tracing";
val category_proof = "Proof";

type pgiptype = string;
val pgipbool = "pgipbool";
val pgipint = "pgipint";
val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
val pgipstring = "pgipstring";

type preference =
 {name: string,
  descr: string,
  default: string,
  pgiptype: pgiptype,
  get: unit -> string,
  set: string -> unit};


(* global preferences *)

local
  val preferences =
    Synchronized.var "ProofGeneral.preferences"
      ([(category_display, []),
        (category_advanced_display, []),
        (category_tracing, []),
        (category_proof, [])]: (category * preference list) list);
in

fun add_preference category (pref: preference) =
  Synchronized.change preferences (map (fn (cat, prefs) =>
    if cat <> category then (cat, prefs)
    else
      if exists (fn {name, ...} => name = #name pref) prefs
      then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
      else (cat, prefs @ [pref])));

fun get_preferences () = Synchronized.value preferences;

end;

fun set_preference name value =
  let val prefs = map (`(#name)) (maps snd (get_preferences ())) in
    (case AList.lookup (op =) prefs name of
      SOME {set, ...} => set value
    | NONE => error ("Unknown prover preference: " ^ quote name))
  end;


(* raw preferences *)

fun preference_raw category raw_get raw_set typ name descr =
  let
    fun get () = CRITICAL raw_get;
    fun set x = CRITICAL (fn () => raw_set x);
    val pref = {name = name, descr = descr, pgiptype = typ, get = get, set = set, default = get ()};
  in add_preference category pref end;

fun preference_ref category read write typ r =
  preference_raw category (fn () => read (! r)) (fn x => r := write x) typ;

fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
fun preference_string category = preference_ref category I I pgipstring;


(* system options *)

fun preference_option category option_name pgip_name descr =
  let
    val typ = Options.default_typ option_name;
    val pgiptype =
      if typ = Options.boolT then pgipbool
      else if typ = Options.intT then pgipint
      else if typ = Options.realT then pgipfloat
      else pgipstring;
  in
    add_preference category
     {name = pgip_name,
      descr = descr,
      default = Options.get_default option_name,
      pgiptype = pgiptype,
      get = fn () => Options.get_default option_name,
      set = Options.put_default option_name}
  end;


(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)

local

fun get_attr attrs name =
  (case Properties.get attrs name of
    SOME value => value
  | NONE => raise Fail ("Missing attribute: " ^ quote name));

fun attr x y = [(x, y)] : XML.attributes;

fun opt_attr _ NONE = []
  | opt_attr name (SOME value) = attr name value;

val pgip_id = "dummy";
val pgip_serial = Synchronized.counter ();

fun output_pgip refid refseq content =
  XML.Elem (("pgip",
    attr "tag" "Isabelle/Isar" @
    attr "id" pgip_id @
    opt_attr "destid" refid @
    attr "class" "pg" @
    opt_attr "refid" refid @
    attr "refseq" refseq @
    attr "seq" (string_of_int (pgip_serial ()))), content)
  |> XML.string_of
  |> Output.urgent_message;


fun invalid_pgip () = raise Fail "Invalid PGIP packet";

fun haspref ({name, descr, default, pgiptype, ...}: preference) =
  XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
    [XML.Elem ((pgiptype, []), [])]);

fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
      get_preferences () |> List.app (fn (category, prefs) =>
        output_pgip refid refseq
          [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
  | process_element _ _ (XML.Elem (("setpref", attrs), data)) =
      let
        val name =
          (case Properties.get attrs "name" of
            SOME name => name
          | NONE => invalid_pgip ());
        val value = XML.content_of data;
      in set_preference name value end
  | process_element _ _ _ = invalid_pgip ();

in

fun process_pgip str =
  (case XML.parse str of<commit_msg>more standard Isabelle/ML structures for global preferences; allow to add categories later on; allow to redefine preferences as usual for global tables, e.g. after reloading ML modules;<commit_after>(*  Title:      Pure/Tools/proof_general.ML
    Author:     <NAME>
    Author:     Makarius

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

signature PROOF_GENERAL =
sig
  type category = string
  val category_display: category
  val category_advanced_display: category
  val category_tracing: category
  val category_proof: category
  type pgiptype = string
  val pgipbool: pgiptype
  val pgipint: pgiptype
  val pgipfloat: pgiptype
  val pgipstring: pgiptype
  val preference_raw: category ->
    (unit -> string) -> (string -> unit) -> string -> string -> string -> unit
  val preference_bool: category -> bool Unsynchronized.ref -> string -> string -> unit
  val preference_int: category -> int Unsynchronized.ref -> string -> string -> unit
  val preference_real: category -> real Unsynchronized.ref -> string -> string -> unit
  val preference_string: category -> string Unsynchronized.ref -> string -> string -> unit
  val preference_option: category -> string -> string -> string -> unit
  structure ThyLoad: sig val add_path: string -> unit end
  val thm_deps: bool Unsynchronized.ref
  val proof_generalN: string
  val init: unit -> unit
end;

structure ProofGeneral: PROOF_GENERAL =
struct

(** preferences **)

(* type preference *)

type category = string;
val category_display = "Display";
val category_advanced_display = "Advanced Display";
val category_tracing = "Tracing";
val category_proof = "Proof";

type pgiptype = string;
val pgipbool = "pgipbool";
val pgipint = "pgipint";
val pgipfloat = "pgipint";  (*NB: PG 3.7.x and 4.0 lack pgipfloat, but accept floats as pgipint*)
val pgipstring = "pgipstring";

type preference =
 {category: string,
  descr: string,
  default: string,
  pgiptype: pgiptype,
  get: unit -> string,
  set: string -> unit};


(* global preferences *)

local
  val preferences =
    Synchronized.var "ProofGeneral.preferences" ([]: (string * preference) list);
in

fun add_preference name pref =
  Synchronized.change preferences (fn prefs =>
   (if not (AList.defined (op =) prefs name) then ()
    else warning ("Redefining ProofGeneral preference: " ^ quote name);
    AList.update (op =) (name, pref) prefs));

fun set_preference name value =
  (case AList.lookup (op =) (Synchronized.value preferences) name of
    SOME {set, ...} => set value
  | NONE => error ("Unknown ProofGeneral preference: " ^ quote name));

fun all_preferences () =
  rev (Synchronized.value preferences)
  |> map (fn (name, {category, descr, default, pgiptype, ...}) =>
    (category, {name = name, descr = descr, default = default, pgiptype = pgiptype}))
  |> AList.group (op =);

end;



(* raw preferences *)

fun preference_raw category raw_get raw_set typ name descr =
  let
    fun get () = CRITICAL raw_get;
    fun set x = CRITICAL (fn () => raw_set x);
  in
    add_preference name
      {category = category, descr = descr, pgiptype = typ, get = get, set = set, default = get ()}
  end;

fun preference_ref category read write typ r =
  preference_raw category (fn () => read (! r)) (fn x => r := write x) typ;

fun preference_bool category = preference_ref category Markup.print_bool Markup.parse_bool pgipbool;
fun preference_int category = preference_ref category Markup.print_int Markup.parse_int pgipint;
fun preference_real category = preference_ref category Markup.print_real Markup.parse_real pgipfloat;
fun preference_string category = preference_ref category I I pgipstring;


(* system options *)

fun preference_option category option_name pgip_name descr =
  let
    val typ = Options.default_typ option_name;
    val pgiptype =
      if typ = Options.boolT then pgipbool
      else if typ = Options.intT then pgipint
      else if typ = Options.realT then pgipfloat
      else pgipstring;
  in
    add_preference pgip_name
     {category = category,
      descr = descr,
      default = Options.get_default option_name,
      pgiptype = pgiptype,
      get = fn () => Options.get_default option_name,
      set = Options.put_default option_name}
  end;


(* minimal PGIP support for <askprefs>, <haspref>, <setpref> *)

local

fun get_attr attrs name =
  (case Properties.get attrs name of
    SOME value => value
  | NONE => raise Fail ("Missing attribute: " ^ quote name));

fun attr x y = [(x, y)] : XML.attributes;

fun opt_attr _ NONE = []
  | opt_attr name (SOME value) = attr name value;

val pgip_id = "dummy";
val pgip_serial = Synchronized.counter ();

fun output_pgip refid refseq content =
  XML.Elem (("pgip",
    attr "tag" "Isabelle/Isar" @
    attr "id" pgip_id @
    opt_attr "destid" refid @
    attr "class" "pg" @
    opt_attr "refid" refid @
    attr "refseq" refseq @
    attr "seq" (string_of_int (pgip_serial ()))), content)
  |> XML.string_of
  |> Output.urgent_message;


fun invalid_pgip () = raise Fail "Invalid PGIP packet";

fun haspref {name, descr, default, pgiptype} =
  XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
    [XML.Elem ((pgiptype, []), [])]);

fun process_element refid refseq (XML.Elem (("askprefs", _), _)) =
      all_preferences () |> List.app (fn (category, prefs) =>
        output_pgip refid refseq
          [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
  | process_element _ _ (XML.Elem (("setpref", attrs), data)) =
      let
        val name =
          (case Properties.get attrs "name" of
            SOME name => name
          | NONE => invalid_pgip ());
        val value = XML.content_of data;
      in set_preference name value end
  | process_element _ _ _ = invalid_pgip ();

in

fun process_pgip str =
  (case XML.parse str of
{'fraction_non_alphanumeric': 0.11452346229733208, 'fraction_numerical': 0.0006862829201338251, 'mean_word_length': 3.5379525107045544, 'pattern_counts': {'":': 0, '<': 12, '<?xml version=': 0, '>': 110, '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': '4530888', 'n_tokens_mistral': 3739, 'n_tokens_neox': 3721, 'n_words': 1185}