<commit_before>(*:wrap=hard:maxLineLen=78:*)

theory JEdit
imports Base
begin

chapter {* Introduction *}

section {* Concepts and terminology *}

text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
  proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
  \emph{asynchronous user interaction}
  \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
  document-oriented approach to \emph{continuous proof processing}
  \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
  components are fit together in order to make this work. The main
  building blocks are as follows.

  \begin{description}

  \item [PIDE] is a general framework for Prover IDEs based on
  Isabelle/Scala. It is built around a concept of parallel and
  asynchronous document processing, which is supported natively by the
  parallel proof engine that is implemented in Isabelle/ML. The prover
  discontinues the traditional TTY-based command loop, and supports
  direct editing of formal source text with rich formal markup for GUI
  rendering.

  \item [Isabelle/ML] is the implementation and extension language of
  Isabelle, see also \cite{isabelle-implementation}. It is integrated
  into the logical context of Isabelle/Isar and allows to manipulate
  logical entities directly. Arbitrary add-on tools may be implemented
  for object-logics such as Isabelle/HOL.

  \item [Isabelle/Scala] is the system programming language of
  Isabelle. It extends the pure logical environment of Isabelle/ML
  towards the ``real world'' of graphical user interfaces, text
  editors, IDE frameworks, web services etc.  Special infrastructure
  allows to transfer algebraic datatypes and formatted text easily
  between ML and Scala, using asynchronous protocol commands.

  \item [jEdit] is a sophisticated text editor implemented in
  Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
  by plugins written in languages that work on the JVM, e.g.\
  Scala\footnote{\url{http://www.scala-lang.org/}}.

  \item [Isabelle/jEdit] is the main example application of the PIDE
  framework and the default user-interface for Isabelle. It targets
  both beginners and experts. Technically, Isabelle/jEdit combines a
  slightly modified version of the jEdit code base with a special
  plugin for Isabelle, integrated as standalone application for the
  main operating system platforms: Linux, Windows, Mac OS X.

  \end{description}

  The subtle differences of Isabelle/ML versus Standard ML,
  Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
  taken into account when discussing any of these PIDE building blocks
  in public forums, mailing lists, or even scientific publications.
  *}


section {* The Isabelle/jEdit Prover IDE *}

text {*
  \begin{figure}[htb]
  \begin{center}
  \includegraphics[width=\textwidth]{isabelle-jedit}
  \end{center}
  \caption{The Isabelle/jEdit Prover IDE}
  \label{fig:isabelle-jedit}
  \end{figure}

  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
  plugins for the well-known jEdit text editor
  \url{http://www.jedit.org}, according to the following principles.

  \begin{itemize}

  \item The original jEdit look-and-feel is generally preserved,
  although some default properties are changed to accommodate Isabelle
  (e.g.\ the text area font).

  \item Formal Isabelle/Isar text is checked asynchronously while
  editing.  The user is in full command of the editor, and the prover
  refrains from locking portions of the buffer.

  \item Prover feedback works via colors, boxes, squiggly underline,
  hyperlinks, popup windows, icons, clickable output --- all based on
  semantic markup produced by Isabelle in the background.

  \item Using the mouse together with the modifier key @{verbatim
  CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
  additional formal content via tooltips and/or hyperlinks.

  \item Formal output (in popups etc.) may be explored recursively,
  using the same techniques as in the editor source buffer.

  \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
  organized by the Dockable Window Manager of jEdit, which also allows
  multiple floating instances of each window class.

  \item The prover process and source files are managed on the editor
  side.  The prover operates on timeless and stateless document
  content as provided via Isabelle/Scala.

  \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
  access to a selection of Isabelle/Scala options and its persistent
  preferences, usually with immediate effect on the prover back-end or
  editor front-end.

  \item The logic image of the prover session may be specified within
  Isabelle/jEdit.  The new image is provided automatically by the
  Isabelle build tool after restart of the application.

  \end{itemize}
*}


subsection {* Documentation *}

text {* Regular jEdit documentation is accessible via its @{verbatim
  Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
  \emph{User's Guide} and \emph{Frequently Asked Questions} for this
  sophisticated text editor.

  Most of this information about jEdit is relevant for Isabelle/jEdit
  as well, but one needs to keep in mind that defaults sometimes
  differ, and the official jEdit documentation does not know about the
  Isabelle plugin with its special support for theory editing.
*}


subsection {* Plugins *}

text {* The \emph{Plugin Manager} of jEdit allows to augment editor
  functionality by JVM modules (jars) that are provided by the central
  plugin repository, which is accessible via various mirror sites.

  Connecting to the plugin server infrastructure of the jEdit project
  allows to update bundled plugins or to add further functionality.
  This needs to be done with the usual care for such an open bazaar of
  contributions. Arbitrary combinations of add-on features are apt to
  cause problems.  It is advisable to start with the default
  configuration of Isabelle/jEdit and develop some understanding how
  it is supposed to work, before loading additional plugins at a grand
  scale.

  \medskip The main \emph{Isabelle} plugin is an integral part of
  Isabelle/jEdit and needs to remain active at all times! A few
  additional plugins are bundled with Isabelle/jEdit for convenience
  or out of necessity, notably \emph{Console} with its Isabelle/Scala
  sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
  for document tree structure.  The \emph{ErrorList} plugin is
  required by \emph{SideKick}, but not used specifically in
  Isabelle/jEdit. *}


subsection {* Options *}

text {* Both jEdit and Isabelle have distinctive management of
  persistent options.

  Regular jEdit options are accessible via the dialog for
  \emph{Plugins / Plugin Options}, which is also accessible via
  \emph{Utilities / Global Options}.  Changed properties are stored in
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"}.  In
  contrast, Isabelle system options are managed by Isabelle/Scala and
  changed values stored in @{file_unchecked
  "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
  properties.  See also \cite{isabelle-sys}, especially the coverage
  of sessions and command-line tools like @{tool build} or @{tool
  options}.

  Those Isabelle options that are declared as \textbf{public} are
  configurable in jEdit via \emph{Plugin Options / Isabelle /
  General}.  Moreover, there are various options for rendering of
  document content, which are configurable via \emph{Plugin Options /
  Isabelle / Rendering}.  Thus \emph{Plugin Options / Isabelle} in
  jEdit provides a view on a subset of Isabelle system options.  Note
  that some of these options affect general parameters that are
  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option
  threads} or @{system_option parallel_proofs} for the Isabelle build
  tool \cite{isabelle-sys}.

  \medskip All options are loaded on startup and saved on shutdown of
  Isabelle/jEdit.  Editing the machine-generated @{file_unchecked
  "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
  "$ISABELLE_HOME_USER/etc/preferences"} manually while the
  application is running is likely to cause surprise due to lost
  update!  *}


subsection {* Keymaps *}

text {* Keyboard shortcuts used to be managed as jEdit properties in
  the past, but recent versions (2013) have a separate concept of
  \emph{keymap} that is configurable via \emph{Global Options /
  Shortcuts}.  The @{verbatim imported} keymap is derived from the
  initial environment of properties that is available at the first
  start of the editor; afterwards the keymap file takes precedence.

  This is relevant for Isabelle/jEdit due to various fine-tuning of
  default properties, and additional keyboard shortcuts for Isabelle
  specific functionality. Users may change their keymap later, but
  need to copy Isabelle-specific key bindings manually (see also
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}).  *}


subsection {* Look-and-feel *}

text {* jEdit is a Java/AWT/Swing application with some ambition to
  support ``native'' look-and-feel on all platforms, within the limits
  of what Oracle as Java provider and major operating system
  distributors allow (see also \secref{sec:problems}).

  Isabelle/jEdit enables platform-specific look-and-feel by default as
  follows:

  \begin{description}

  \item[Linux] The platform-independent \emph{Nimbus} is used by
  default.

  \emph{GTK+} works under the side-condition that the overall GTK
  theme is selected in a Swing-friendly way.\footnote{GTK support in
  Java/Swing was once marketed aggressively by Sun, but never quite
  finished, and is today (2013) lagging a bit behind further
  development of Swing and GTK.}

  \item[Windows] Regular \emph{Windows} is used by default, but
  \emph{Windows Classic} also works.

  \item[Mac OS X] Regular \emph{Mac OS X} is used by default.

  Moreover the bundled \emph{MacOSX} plugin provides various functions
  that are expected from applications on that particular platform:
  quit from menu or dock, preferences menu, drag-and-drop of text
  files on the application, full-screen mode for main editor windows
  etc.

  \end{description}

  Users may experiment with different look-and-feels, but need to keep
  in mind that this extra variance of GUI functionality is unlikely to
  work in arbitrary combinations.  The platform-independent
  \emph{Nimbus} and \emph{Metal} should always work.  The historic
  \emph{CDE/Motif} is better avoided.

  After changing the look-and-feel in \emph{Global Options /
  Appearance}, it is advisable to restart Isabelle/jEdit in order to
  take full effect.  *}


chapter {* Prover IDE functionality *}

section {* File-system access *}

text {* File specifications in jEdit follow various formats and
  conventions according to \emph{Virtual File Systems}, which may be
  also provided by additional plugins.  This allows to access remote
  files via the @{verbatim "http:"} protocol prefix, for example.
  Isabelle/jEdit attempts to work with the file-system access model of
  jEdit as far as possible.  In particular, theory sources are passed
  directly from the editor to the prover, without indirection via
  files.

  Despite the flexibility of URLs in jEdit, local files are
  particularly important and are accessible without protocol prefix.
  Here the path notation is that of the Java Virtual Machine on the
  underlying platform.  On Windows the preferred form uses
  backslashes, but happens to accept Unix/POSIX forward slashes, too.
  Further differences arise due to drive letters and network shares.

  The Java notation for files needs to be distinguished from the one
  of Isabelle, which uses POSIX notation with forward slashes on
  \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
  file-system access.}  Moreover, environment variables from the
  Isabelle process may be used freely, e.g.\ @{file
  "$ISABELLE_HOME/etc/symbols"} or @{file
  "$ISABELLE_JDK_HOME/README.html"}.  There are special shortcuts:
  @{file "~"} for @{file "$USER_HOME"} and @{file "~~"} for @{file
  "$ISABELLE_HOME"}.

  \medskip Since jEdit happens to support environment variables within
  file specifications as well, it is natural to use similar notation
  within the editor, e.g.\ in the file-browser.  This does not work in
  full generality, though, due to the bias of jEdit towards
  platform-specific notation and of Isabelle towards POSIX.  Moreover,
  the Isabelle settings environment is not yet active when starting
  Isabelle/jEdit via its standard application wrapper (in contrast to
  @{verbatim "isabelle jedit"} run from the command line).

  For convenience, Isabelle/jEdit imitates at least @{verbatim
  "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the
  Java process environment, in order to allow easy access to these
  important places from the editor.

  Moreover note that path specifications in prover input or output
  usually include formal markup that turns it into a hyperlink (see<commit_msg>compile on Windows (clone of d04576557400);<commit_after>(*:wrap=hard:maxLineLen=78:*)

theory JEdit
imports Base
begin

chapter {* Introduction *}

section {* Concepts and terminology *}

text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
  proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
  \emph{asynchronous user interaction}
  \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
  document-oriented approach to \emph{continuous proof processing}
  \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
  components are fit together in order to make this work. The main
  building blocks are as follows.

  \begin{description}

  \item [PIDE] is a general framework for Prover IDEs based on
  Isabelle/Scala. It is built around a concept of parallel and
  asynchronous document processing, which is supported natively by the
  parallel proof engine that is implemented in Isabelle/ML. The prover
  discontinues the traditional TTY-based command loop, and supports
  direct editing of formal source text with rich formal markup for GUI
  rendering.

  \item [Isabelle/ML] is the implementation and extension language of
  Isabelle, see also \cite{isabelle-implementation}. It is integrated
  into the logical context of Isabelle/Isar and allows to manipulate
  logical entities directly. Arbitrary add-on tools may be implemented
  for object-logics such as Isabelle/HOL.

  \item [Isabelle/Scala] is the system programming language of
  Isabelle. It extends the pure logical environment of Isabelle/ML
  towards the ``real world'' of graphical user interfaces, text
  editors, IDE frameworks, web services etc.  Special infrastructure
  allows to transfer algebraic datatypes and formatted text easily
  between ML and Scala, using asynchronous protocol commands.

  \item [jEdit] is a sophisticated text editor implemented in
  Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
  by plugins written in languages that work on the JVM, e.g.\
  Scala\footnote{\url{http://www.scala-lang.org/}}.

  \item [Isabelle/jEdit] is the main example application of the PIDE
  framework and the default user-interface for Isabelle. It targets
  both beginners and experts. Technically, Isabelle/jEdit combines a
  slightly modified version of the jEdit code base with a special
  plugin for Isabelle, integrated as standalone application for the
  main operating system platforms: Linux, Windows, Mac OS X.

  \end{description}

  The subtle differences of Isabelle/ML versus Standard ML,
  Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
  taken into account when discussing any of these PIDE building blocks
  in public forums, mailing lists, or even scientific publications.
  *}


section {* The Isabelle/jEdit Prover IDE *}

text {*
  \begin{figure}[htb]
  \begin{center}
  \includegraphics[width=\textwidth]{isabelle-jedit}
  \end{center}
  \caption{The Isabelle/jEdit Prover IDE}
  \label{fig:isabelle-jedit}
  \end{figure}

  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
  plugins for the well-known jEdit text editor
  \url{http://www.jedit.org}, according to the following principles.

  \begin{itemize}

  \item The original jEdit look-and-feel is generally preserved,
  although some default properties are changed to accommodate Isabelle
  (e.g.\ the text area font).

  \item Formal Isabelle/Isar text is checked asynchronously while
  editing.  The user is in full command of the editor, and the prover
  refrains from locking portions of the buffer.

  \item Prover feedback works via colors, boxes, squiggly underline,
  hyperlinks, popup windows, icons, clickable output --- all based on
  semantic markup produced by Isabelle in the background.

  \item Using the mouse together with the modifier key @{verbatim
  CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
  additional formal content via tooltips and/or hyperlinks.

  \item Formal output (in popups etc.) may be explored recursively,
  using the same techniques as in the editor source buffer.

  \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
  organized by the Dockable Window Manager of jEdit, which also allows
  multiple floating instances of each window class.

  \item The prover process and source files are managed on the editor
  side.  The prover operates on timeless and stateless document
  content as provided via Isabelle/Scala.

  \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
  access to a selection of Isabelle/Scala options and its persistent
  preferences, usually with immediate effect on the prover back-end or
  editor front-end.

  \item The logic image of the prover session may be specified within
  Isabelle/jEdit.  The new image is provided automatically by the
  Isabelle build tool after restart of the application.

  \end{itemize}
*}


subsection {* Documentation *}

text {* Regular jEdit documentation is accessible via its @{verbatim
  Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
  \emph{User's Guide} and \emph{Frequently Asked Questions} for this
  sophisticated text editor.

  Most of this information about jEdit is relevant for Isabelle/jEdit
  as well, but one needs to keep in mind that defaults sometimes
  differ, and the official jEdit documentation does not know about the
  Isabelle plugin with its special support for theory editing.
*}


subsection {* Plugins *}

text {* The \emph{Plugin Manager} of jEdit allows to augment editor
  functionality by JVM modules (jars) that are provided by the central
  plugin repository, which is accessible via various mirror sites.

  Connecting to the plugin server infrastructure of the jEdit project
  allows to update bundled plugins or to add further functionality.
  This needs to be done with the usual care for such an open bazaar of
  contributions. Arbitrary combinations of add-on features are apt to
  cause problems.  It is advisable to start with the default
  configuration of Isabelle/jEdit and develop some understanding how
  it is supposed to work, before loading additional plugins at a grand
  scale.

  \medskip The main \emph{Isabelle} plugin is an integral part of
  Isabelle/jEdit and needs to remain active at all times! A few
  additional plugins are bundled with Isabelle/jEdit for convenience
  or out of necessity, notably \emph{Console} with its Isabelle/Scala
  sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
  for document tree structure.  The \emph{ErrorList} plugin is
  required by \emph{SideKick}, but not used specifically in
  Isabelle/jEdit. *}


subsection {* Options *}

text {* Both jEdit and Isabelle have distinctive management of
  persistent options.

  Regular jEdit options are accessible via the dialog for
  \emph{Plugins / Plugin Options}, which is also accessible via
  \emph{Utilities / Global Options}.  Changed properties are stored in
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"}.  In
  contrast, Isabelle system options are managed by Isabelle/Scala and
  changed values stored in @{file_unchecked
  "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
  properties.  See also \cite{isabelle-sys}, especially the coverage
  of sessions and command-line tools like @{tool build} or @{tool
  options}.

  Those Isabelle options that are declared as \textbf{public} are
  configurable in jEdit via \emph{Plugin Options / Isabelle /
  General}.  Moreover, there are various options for rendering of
  document content, which are configurable via \emph{Plugin Options /
  Isabelle / Rendering}.  Thus \emph{Plugin Options / Isabelle} in
  jEdit provides a view on a subset of Isabelle system options.  Note
  that some of these options affect general parameters that are
  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option
  threads} or @{system_option parallel_proofs} for the Isabelle build
  tool \cite{isabelle-sys}.

  \medskip All options are loaded on startup and saved on shutdown of
  Isabelle/jEdit.  Editing the machine-generated @{file_unchecked
  "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
  "$ISABELLE_HOME_USER/etc/preferences"} manually while the
  application is running is likely to cause surprise due to lost
  update!  *}


subsection {* Keymaps *}

text {* Keyboard shortcuts used to be managed as jEdit properties in
  the past, but recent versions (2013) have a separate concept of
  \emph{keymap} that is configurable via \emph{Global Options /
  Shortcuts}.  The @{verbatim imported} keymap is derived from the
  initial environment of properties that is available at the first
  start of the editor; afterwards the keymap file takes precedence.

  This is relevant for Isabelle/jEdit due to various fine-tuning of
  default properties, and additional keyboard shortcuts for Isabelle
  specific functionality. Users may change their keymap later, but
  need to copy Isabelle-specific key bindings manually (see also
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}).  *}


subsection {* Look-and-feel *}

text {* jEdit is a Java/AWT/Swing application with some ambition to
  support ``native'' look-and-feel on all platforms, within the limits
  of what Oracle as Java provider and major operating system
  distributors allow (see also \secref{sec:problems}).

  Isabelle/jEdit enables platform-specific look-and-feel by default as
  follows:

  \begin{description}

  \item[Linux] The platform-independent \emph{Nimbus} is used by
  default.

  \emph{GTK+} works under the side-condition that the overall GTK
  theme is selected in a Swing-friendly way.\footnote{GTK support in
  Java/Swing was once marketed aggressively by Sun, but never quite
  finished, and is today (2013) lagging a bit behind further
  development of Swing and GTK.}

  \item[Windows] Regular \emph{Windows} is used by default, but
  \emph{Windows Classic} also works.

  \item[Mac OS X] Regular \emph{Mac OS X} is used by default.

  Moreover the bundled \emph{MacOSX} plugin provides various functions
  that are expected from applications on that particular platform:
  quit from menu or dock, preferences menu, drag-and-drop of text
  files on the application, full-screen mode for main editor windows
  etc.

  \end{description}

  Users may experiment with different look-and-feels, but need to keep
  in mind that this extra variance of GUI functionality is unlikely to
  work in arbitrary combinations.  The platform-independent
  \emph{Nimbus} and \emph{Metal} should always work.  The historic
  \emph{CDE/Motif} is better avoided.

  After changing the look-and-feel in \emph{Global Options /
  Appearance}, it is advisable to restart Isabelle/jEdit in order to
  take full effect.  *}


chapter {* Prover IDE functionality *}

section {* File-system access *}

text {* File specifications in jEdit follow various formats and
  conventions according to \emph{Virtual File Systems}, which may be
  also provided by additional plugins.  This allows to access remote
  files via the @{verbatim "http:"} protocol prefix, for example.
  Isabelle/jEdit attempts to work with the file-system access model of
  jEdit as far as possible.  In particular, theory sources are passed
  directly from the editor to the prover, without indirection via
  files.

  Despite the flexibility of URLs in jEdit, local files are
  particularly important and are accessible without protocol prefix.
  Here the path notation is that of the Java Virtual Machine on the
  underlying platform.  On Windows the preferred form uses
  backslashes, but happens to accept Unix/POSIX forward slashes, too.
  Further differences arise due to drive letters and network shares.

  The Java notation for files needs to be distinguished from the one
  of Isabelle, which uses POSIX notation with forward slashes on
  \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
  file-system access.}  Moreover, environment variables from the
  Isabelle process may be used freely, e.g.\ @{file
  "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}.
  There are special shortcuts: @{file "~"} for @{file "$USER_HOME"}
  and @{file "~~"} for @{file "$ISABELLE_HOME"}.

  \medskip Since jEdit happens to support environment variables within
  file specifications as well, it is natural to use similar notation
  within the editor, e.g.\ in the file-browser.  This does not work in
  full generality, though, due to the bias of jEdit towards
  platform-specific notation and of Isabelle towards POSIX.  Moreover,
  the Isabelle settings environment is not yet active when starting
  Isabelle/jEdit via its standard application wrapper (in contrast to
  @{verbatim "isabelle jedit"} run from the command line).

  For convenience, Isabelle/jEdit imitates at least @{verbatim
  "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the
  Java process environment, in order to allow easy access to these
  important places from the editor.

  Moreover note that path specifications in prover input or output
  usually include formal markup that turns it into a hyperlink (see
{'fraction_non_alphanumeric': 0.06034285714285714, 'fraction_numerical': 0.003085714285714286, 'mean_word_length': 4.149274225186348, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 6, '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': '6309050', 'n_tokens_mistral': 7337, 'n_tokens_neox': 7067, 'n_words': 3360}