<commit_before>/*  Title:      Pure/Tools/isabelle_process.ML
    Author:     Makarius
    Options:    :folding=explicit:collapseFolds=1:

Isabelle process management -- always reactive due to multi-threaded I/O.
*/

package isabelle

import java.util.Properties
import java.util.concurrent.LinkedBlockingQueue
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
  InputStream, OutputStream, IOException}


object IsabelleProcess {

  /* results */

  object Kind extends Enumeration {
    //{{{ values and codes
    // internal system notification
    val SYSTEM = Value("SYSTEM")
    // Posix channels/events
    val STDIN = Value("STDIN")
    val STDOUT = Value("STDOUT")
    val SIGNAL = Value("SIGNAL")
    val EXIT = Value("EXIT")
    // Isabelle messages
    val INIT = Value("INIT")
    val STATUS = Value("STATUS")
    val WRITELN = Value("WRITELN")
    val PRIORITY = Value("PRIORITY")
    val TRACING = Value("TRACING")
    val WARNING = Value("WARNING")
    val ERROR = Value("ERROR")
    val DEBUG = Value("DEBUG")
    // messages codes
    val code = Map(
      ('A' : Int) -> Kind.INIT,
      ('B' : Int) -> Kind.STATUS,
      ('C' : Int) -> Kind.WRITELN,
      ('D' : Int) -> Kind.PRIORITY,
      ('E' : Int) -> Kind.TRACING,
      ('F' : Int) -> Kind.WARNING,
      ('G' : Int) -> Kind.ERROR,
      ('H' : Int) -> Kind.DEBUG,
      ('0' : Int) -> Kind.SYSTEM,
      ('1' : Int) -> Kind.STDIN,
      ('2' : Int) -> Kind.STDOUT,
      ('3' : Int) -> Kind.SIGNAL,
      ('4' : Int) -> Kind.EXIT)
    //}}}
    def is_raw(kind: Value) =
      kind == STDOUT
    def is_control(kind: Value) =
      kind == SYSTEM ||
      kind == SIGNAL ||
      kind == EXIT
    def is_system(kind: Value) =
      kind == SYSTEM ||
      kind == STDIN ||
      kind == SIGNAL ||
      kind == EXIT ||
      kind == STATUS
  }

  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
    override def toString = {
      val res = XML.content(YXML.parse_failsafe(result)).mkString
      if (props == null) kind.toString + " [[" + res + "]]"
      else kind.toString + " " + props.toString + " [[" + res + "]]"
    }
    def is_raw = Kind.is_raw(kind)
    def is_control = Kind.is_control(kind)
    def is_system = Kind.is_system(kind)
  }

}


class IsabelleProcess(isabelle_system: IsabelleSystem,
  results: EventBus[IsabelleProcess.Result], args: String*)
{
  import IsabelleProcess._


  /* demo constructor */

  def this(args: String*) =
    this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)


  /* process information */

  private var proc: Process = null
  private var closing = false
  private var pid: String = null
  private var the_session: String = null
  def session() = the_session
<commit_msg>Result.toString: XML output of status messages;<commit_after>/*  Title:      Pure/Tools/isabelle_process.ML
    Author:     Makarius
    Options:    :folding=explicit:collapseFolds=1:

Isabelle process management -- always reactive due to multi-threaded I/O.
*/

package isabelle

import java.util.Properties
import java.util.concurrent.LinkedBlockingQueue
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
  InputStream, OutputStream, IOException}


object IsabelleProcess {

  /* results */

  object Kind extends Enumeration {
    //{{{ values and codes
    // internal system notification
    val SYSTEM = Value("SYSTEM")
    // Posix channels/events
    val STDIN = Value("STDIN")
    val STDOUT = Value("STDOUT")
    val SIGNAL = Value("SIGNAL")
    val EXIT = Value("EXIT")
    // Isabelle messages
    val INIT = Value("INIT")
    val STATUS = Value("STATUS")
    val WRITELN = Value("WRITELN")
    val PRIORITY = Value("PRIORITY")
    val TRACING = Value("TRACING")
    val WARNING = Value("WARNING")
    val ERROR = Value("ERROR")
    val DEBUG = Value("DEBUG")
    // messages codes
    val code = Map(
      ('A' : Int) -> Kind.INIT,
      ('B' : Int) -> Kind.STATUS,
      ('C' : Int) -> Kind.WRITELN,
      ('D' : Int) -> Kind.PRIORITY,
      ('E' : Int) -> Kind.TRACING,
      ('F' : Int) -> Kind.WARNING,
      ('G' : Int) -> Kind.ERROR,
      ('H' : Int) -> Kind.DEBUG,
      ('0' : Int) -> Kind.SYSTEM,
      ('1' : Int) -> Kind.STDIN,
      ('2' : Int) -> Kind.STDOUT,
      ('3' : Int) -> Kind.SIGNAL,
      ('4' : Int) -> Kind.EXIT)
    //}}}
    def is_raw(kind: Value) =
      kind == STDOUT
    def is_control(kind: Value) =
      kind == SYSTEM ||
      kind == SIGNAL ||
      kind == EXIT
    def is_system(kind: Value) =
      kind == SYSTEM ||
      kind == STDIN ||
      kind == SIGNAL ||
      kind == EXIT ||
      kind == STATUS
  }

  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
    override def toString = {
      val tree = YXML.parse_failsafe(result)
      val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString
      if (props == null) kind.toString + " [[" + res + "]]"
      else kind.toString + " " + props.toString + " [[" + res + "]]"
    }
    def is_raw = Kind.is_raw(kind)
    def is_control = Kind.is_control(kind)
    def is_system = Kind.is_system(kind)
  }

}


class IsabelleProcess(isabelle_system: IsabelleSystem,
  results: EventBus[IsabelleProcess.Result], args: String*)
{
  import IsabelleProcess._


  /* demo constructor */

  def this(args: String*) =
    this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)


  /* process information */

  private var proc: Process = null
  private var closing = false
  private var pid: String = null
  private var the_session: String = null
  def session() = the_session

{'fraction_non_alphanumeric': 0.1431571578578929, 'fraction_numerical': 0.0021001050052502626, 'mean_word_length': 2.708630759247242, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 29, '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': '114290', 'n_tokens_mistral': 1893, 'n_tokens_neox': 1847, 'n_words': 483}