Ich möchte Source Code mit dem Paket Listing (lstlisting) setzen. Ich verwende Annotationen mit Schlüsselworten in Source Code Kommentaren. Die Annotationssprache ist dem Paket bekannt (ACSL). Leider werden diese Schlüsselworte im Kommentar nicht erkannt und nicht entsprechend gesetzt. Ich habe es auch schon mit der Option "alsolanguage" versucht, ohne Erfolg.

Wie kann ich Listing dazu bringen, auch die Annotationen korrekt umzusetzen?

Unten ein Beispiel. Die Schlüsselworte sind "behavior", "assumes", etc.

Vielen Dank im Voraus

Open in writeLaTeX
//@ ghost unsigned int no_btn_press = 0;

/*@
  @  behavior FewPresses:
  @    assumes no_btn_press < 2;
  @    ensures no_btn_press == \old(no_btn_press) + 1;
  @    ensures \result == 0;
  @  behavior EnoughPresses:
  @    assumes no_btn_press >= 2;
  @    ensures no_btn_press == 0;
  @    ensures \result != 0;
  @  complete behaviors FewPresses,EnoughPresses;
  @  disjoint behaviors FewPresses,EnoughPresses;
  @*/
char btnpress(void);

gefragt 18 Mai '14, 09:48

dordow's gravatar image

dordow
384
Akzeptiert: 66%

bearbeitet 18 Mai '14, 14:35

Clemens's gravatar image

Clemens
19.0k112960

Ist es nicht normal, dass Schlüsselwörter in Kommentaren nicht formatiert werden? Oder verstehe ich die Frage falsch?

(18 Mai '14, 14:40) Clemens

Mein Bauchgefühl sagt auch, Kommentare sollten in ihrer Gestaltung zurücktreten (hellgrau z.B.), damit die wichtige Syntax-Hervorhebung des echten Codes noch besser erkennbar ist. Formatierung von Schlüsselwörtern in Kommentaren lassen sie "aktiv" aussehen, doch sie sind ja wirkungslos, fände ich irritierend.

(18 Mai '14, 14:57) stefan ♦♦

Du kannst Dir den Stil auch komplett selbst definieren. Hier einmal mit dem Stil von openETCS, was Du Dir ja modifizieren kannst:

Open in writeLaTeX
\documentclass[preview,border=5]{standalone}
\usepackage{listings}
\usepackage{xcolor}

%\definecolor{darkred} {rgb}{0.60,0.00,0.00}
\definecolor{coACSLBehavior}    {rgb}{0.30,0.00,0.00}
\definecolor{coASCL}    {rgb}{0.00,0.10,0.00}
\definecolor{coASCLKeyword} {rgb}{0.00,0.10,0.10}
\definecolor{darkgreen} {rgb}{0.00,0.40,0.00}
%\definecolor{red} {rgb}{0.98,0.00,0.00}
\definecolor{darkblue}  {rgb}{0.00,0.00,0.60}
%\definecolor{lightblue} {rgb}{0.60,0.80,1.00}
%\definecolor{lightred} {rgb}{1.00,0.60,0.60}
\definecolor{coCKeyword}    {rgb}{0.00,0.00,0.60}

\lstdefinestyle{acsl-block}{
  emph=[1]{assert, assumes, assigns, axiom, axiomatic, decreases, ensures,
           ghost, invariant, lemma, logic, loop, predicate,
           reads, requires, variant},
  emphstyle=[1]{\bfseries\color{coASCLKeyword}},
  emph=[2]{behavior, behaviors, complete, disjoint, for:},
  emphstyle=[2]{\bfseries\color{coACSLBehavior}},
  emph=[3]{typedef, int, char, integer, real, bool, size_type, value_type,
           uint8_t, uint64_t},
  emphstyle=[3]{\bfseries\color{coCKeyword}},
  escapeinside={//`}{`//},
  morecomment=*[l][\color{coASCL}]{//@},
  morecomment=*[s][\color{coASCL}]{/*@}{*/},
  moredelim=*[is][\bfseries]{|*}{*|},
  %emphstyle=[3]{\ttfamily}
}
\begin{document}
\begin{lstlisting}[style=acsl-block]
//@ ghost unsigned int no_btn_press = 0;

/*@
  @  behavior FewPresses:
  @    assumes no_btn_press < 2;
  @    ensures no_btn_press == \old(no_btn_press) + 1;
  @    ensures \result == 0;
  @  behavior EnoughPresses:
  @    assumes no_btn_press >= 2;
  @    ensures no_btn_press == 0;
  @    ensures \result != 0;
  @  complete behaviors FewPresses,EnoughPresses;
  @  disjoint behaviors FewPresses,EnoughPresses;
  @*/
char btnpress(void);
\end{lstlisting}
\end{document}

Listing

Permanenter link

beantwortet 18 Mai '14, 13:14

stefan's gravatar image

stefan ♦♦
5.8k12134

Das ist genau was ich brauchte, vielen Dank.

(18 Mai '14, 15:52) dordow
Deine Antwort auf die Frage (nicht auf andere Antworten)
Knebel-Vorschau

Folge dieser Frage

Per E-Mail:

Wenn Du Dich anmeldest, kannst Du Updates hier abonnieren

Per RSS:

Antworten

Antworten und Kommentare

Aktuelle Buch-Infos

LaTeX Cookbook

LaTeX Beginners Guide

Limitierter Rabatt ebook
50% Coupon code tDRet6Y

Markdown-Grundlagen

  • *kursiv* oder _kursiv_
  • **Fett** oder __Fett__
  • Link:[Text](http://url.com/ "Titel")
  • Bild?![alt Text](/path/img.jpg "Titel")
  • nummerierte Liste: 1. Foo 2. Bar
  • zum Hinzufügen ein Zeilenumbruchs füge einfach zwei Leerzeichen an die Stelle ein, an der die neue Zeile sein soll.
  • grundlegende HTML-Tags werden ebenfalls unterstützt

Zugeordnete Themen:

×15

Frage gestellt: 18 Mai '14, 09:48

Frage wurde angeschaut: 1,895 Mal

Zuletzt aktualisiert: 18 Mai '14, 15:52