% pluscal.tex --- PlusCal language definition for listings -*-latex-*-

% Copyright (C) 2018 Nancy Day <nday@uwaterloo.ca>
% Copyright (C) 2018, 2020 Amin Bandali <bandali@uwaterloo.ca>

% This file is part of Amin Bandali's MMath thesis.

% This thesis is free software: you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation, either version 3 of the License, or
% (at your option) any later version.

% This thesis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.

% You should have received a copy of the GNU General Public License
% along with this thesis.  If not, see <https://www.gnu.org/licenses/>.


\usepackage[formats]{listings}
% Define Language
\lstdefinelanguage{pluscal}{
  % list of keywords
  morekeywords={
    %% PlusCal keywords
    algorithm,
    assert,
    await,
    begin,
    call,
    define,
    do,
    either,
    else,
    elsif,
    end,
    fair,
    variable,
    variables,
    end,
    goto,
    if,
    macro,
    or,
    print,
    procedure,
    process,
    return,
    skip,
    then,
    when,
    while,
    with,
    %% TLA+ keywords
    EXTENDS,
    CONSTANT,
    CONSTANTS,
    VARIABLE,
    VARIABLES,
    ASSUME,
    INSTANCE,
    WITH,
    THEOREM,
    LOCAL,
    TRUE,
    FALSE,
    BOOLEAN,
    Int,
    Nat,
    CHOOSE,
    SUBSET,
    UNION,
    DOMAIN,
    EXCEPT,
    STRING,
    IF,
    THEN,
    ELSE,
    CASE,
    OTHER,
    LET,
    IN,
    ENABLED,
    UNCHANGED,
    MODULE,
    %SF_,
    %WF_,
    % new keywords in TLA+2
    ACTION,
    ASSUMPTION,
    AXIOM,
    BY,
    COROLLARY,
    DEF,
    DEFINE,
    DEFS,
    HAVE,
    HIDE,
    LAMBDA,
    LEMMA,
    NEW,
    OBVIOUS,
    OMITTED,
    ONLY,
    PICK,
    PROOF,
    PROPOSITION,
    PROVE,
    QED,
    RECURSIVE,
    STATE,
    SUFFICES,
    TAKE,
    TEMPORAL,
    USE,
    WITNESS
  },
  sensitive=true, % keywords are case-sensitive
  morecomment=[l]{\\*}, % l is for line comment
  % morecomment=[s]{(*}{*)}, % s is for start and end delimiter
  morestring=[b]" % defines that strings are enclosed in double quotes
}

\lstdefineformat{pluscal}{~={\raise.17ex\hbox{$\scriptstyle\sim$}}}
% Set Language
\lstdefinestyle{pluscal}{
  language={pluscal},
  basicstyle=\footnotesize\ttfamily, % Global Code Style
  captionpos=b, % Position of the Caption (t for top, b for bottom)
  extendedchars=true, % Allows 256 instead of 128 ASCII characters
  format=pluscal,
  tabsize=2, % number of spaces indented when discovering a tab 
  columns=flexible, % make all characters equal width
  keepspaces=true, % does not ignore spaces to fit width, convert tabs to spaces
  showstringspaces=false, % lets spaces in strings appear as real spaces
  breaklines=true, % wrap lines if they don't fit
  %frame=trbl, % draw a frame at the top, right, left and bottom of the listing
  %frameround=tttt, % make the frame round at all four corners
  framesep=4pt, % quarter circle size of the round corners
  numbers=left, % show line numbers at the left
  numberstyle=\footnotesize\ttfamily, % style of the line numbers
  commentstyle=\color{eclipseGreen}, % style of comments
  keywordstyle=\color{cpluscal}, % style of keywords
  stringstyle=\color{eclipseBlue}, % style of strings
  xleftmargin=0.8cm,
  escapeinside={\%*}{*)}          % if you want to add LaTeX within your code
}

\newcommand{\pluscalcode}[1]{\lstinline[style=pluscal, breakatwhitespace, basicstyle=\ttfamily]{#1}}


%% Local Variables:
%% tex-main-file: "../bandali-mmath-thesis.tex"
%% End:
