Searched refs:comment (Results 1 - 25 of 86) sorted by relevance

1234

/seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/holdep/errors/
H A Dcomment_unterm.sml1 val foo = 3 (* comment here
/seL4-l4v-10.1.1/HOL4/src/TeX/
H A DholindexData.sml14 comment : string option,
27 comment = NONE,
38 comment = comment,
48 comment = comment,
60 comment = comment,
70 comment = comment,
[all...]
H A DholindexData.sig9 comment : string option,
44 comment : string option,
H A Dholindex-demo.tex86 \commentHOLtm{unique_id}{comment}
87 \commentHOLty{unique_id}{comment}
88 \commentHOLthm{unique_id}{comment}
131 comment = "some lengthy\\comment
295 % Arg 7 : comment
316 % Arg 6 : comment
361 \commentHOLty{type_id_4}{Some short comment}
/seL4-l4v-10.1.1/isabelle/Admin/
H A Drsyncd.conf11 comment = Isabelle website
15 comment = Isabelle distribution
20 comment = Isabelle website
/seL4-l4v-10.1.1/l4v/isabelle/Admin/
H A Drsyncd.conf11 comment = Isabelle website
15 comment = Isabelle distribution
20 comment = Isabelle website
/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/
H A DmergeGrammarsA2Script.sml5 (* see comment at head of mergeGrammarsA1Script for description of what is
H A DmergeGrammarsBScript.sml3 (* see comment at head of mergeGrammarsA1Script.sml for explanation of
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dupdate_comments.scala4 Update formal comments in outer syntax: \<comment> \<open>...\<close>
18 Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content))
24 if tok.source == "--" || tok.source == Symbol.comment =>
30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) =>
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dupdate_comments.scala4 Update formal comments in outer syntax: \<comment> \<open>...\<close>
18 Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content))
24 if tok.source == "--" || tok.source == Symbol.comment =>
30 case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) =>
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/
H A Dgrammar.scala50 "comment": {
53 "name": "comment.block.isabelle",
55 "patterns": [{ "include": "#comment" }],
73 "include": "#comment"
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/VSCode/src/
H A Dgrammar.scala50 "comment": {
53 "name": "comment.block.isabelle",
55 "patterns": [{ "include": "#comment" }],
73 "include": "#comment"
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/scripts/
H A Dmlpp106 my $comment = 0;
128 elsif ($state eq "comment") {
137 ++$comment;
141 --$comment;
142 if ($comment == 0) { $state = "normal"; }
206 $state = "comment";
207 ++$comment;
212 die "mlpp: too many comment closers.\n"
243 elsif ($state eq "comment") {
244 die "mlpp: EOF inside comment\
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/scripts/
H A Dmlpp106 my $comment = 0;
128 elsif ($state eq "comment") {
137 ++$comment;
141 --$comment;
142 if ($comment == 0) { $state = "normal"; }
206 $state = "comment";
207 ++$comment;
212 die "mlpp: too many comment closers.\n"
243 elsif ($state eq "comment") {
244 die "mlpp: EOF inside comment\
[all...]
/seL4-l4v-10.1.1/seL4/manual/tools/
H A Dgen_invocations.py43 def generate_prototype(interface_name, method_name, method_id, inputs, outputs, comment):
57 return "%s\n%s %s %s(%s);" % (comment, prefix, return_type, name, param_list)
87 for (interface_name, method_name, method_id, inputs, outputs, _, comment) in methods:
89 prototype += generate_prototype(interface_name, method_name, method_id, inputs, outputs, comment)
/seL4-l4v-10.1.1/graph-refine/graph-to-graph/
H A Dconvert_loop_bounds.py77 comment = 'did not find cached result'
79 comment = 'ignore: failed'
80 lbfs[f][head] = (2**30, comment, old_worker)
/seL4-l4v-10.1.1/HOL4/src/ring/src/
H A DnumRingScript.sml34 * of comment. ^^^
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dcomment.scala1 /* Title: Pure/General/comment.scala
14 val COMMENT = Value("formal comment")
20 Set(Symbol.comment, Symbol.comment_decoded,
25 Set(Symbol.comment, Symbol.comment_decoded)
29 def err(): Nothing = error("Malformed formal comment: " + quote(source))
H A Dsymbol.scala488 val comment_decoded = decode(comment)
575 val comment: Symbol = "\\<comment>"
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dcomment.scala1 /* Title: Pure/General/comment.scala
14 val COMMENT = Value("formal comment")
20 Set(Symbol.comment, Symbol.comment_decoded,
25 Set(Symbol.comment, Symbol.comment_decoded)
29 def err(): Nothing = error("Malformed formal comment: " + quote(source))
H A Dsymbol.scala488 val comment_decoded = decode(comment)
575 val comment: Symbol = "\\<comment>"
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/parser.mosmlyacc/
H A DLexer.lex17 val commentStart = ref 0; (* Start of outermost comment being scanned *)
23 val commentDepth = ref 0; (* Current comment nesting *)
/seL4-l4v-10.1.1/isabelle/src/Doc/Eisbach/document/
H A Droot.tex37 \newenvironment{LongComment}[1] % multi-paragraph comment, argument is owner
44 \newenvironment{LongComment}[1]{\expandafter\comment}{\expandafter\endcomment}
/seL4-l4v-10.1.1/l4v/isabelle/src/Doc/Eisbach/document/
H A Droot.tex37 \newenvironment{LongComment}[1] % multi-paragraph comment, argument is owner
44 \newenvironment{LongComment}[1]{\expandafter\comment}{\expandafter\endcomment}
/seL4-l4v-10.1.1/HOL4/src/boss/theory_tests/
H A Dtheory3Script.sml48 (* comment out line above, and it works OK *)

Completed in 267 milliseconds

1234