Searched refs:file (Results 201 - 225 of 645) sorted by relevance

1234567891011>>

/seL4-l4v-master/HOL4/polyml/basis/
H A DFinalPolyML.sml37 The rootFunction has now been pulled out into a separate file and is added on
163 location is the file-name, line number and position. context is an
174 the current file, a byte offset or simply zero.
177 (* The current file being compiled. This is used by the default CPErrorMessageProc
277 SOME (ContextLocation{file,startLine,startPosition,endPosition, ...}) =>
280 file name convert it to ESC-ESC. *)
285 stream(String.translate escapeEscapes file);
414 location={startLine, startPosition, endPosition, file, ...}: PolyML.location,
440 file, (* TODO double any escapes. *) separator,
452 ( (if file
[all...]
/seL4-l4v-master/HOL4/src/HolSat/
H A DSatSolvers.sml2 ** This file contains specifications of the SAT tools that
10 ** notime_run, (* command to invoke solver on a file *)
11 ** time_run, (* command to invoke on a file and time *)
/seL4-l4v-master/HOL4/Manual/Translations/IT/Tutorial/
H A Dintro.tex30 file \texttt{tar} sia stato estratto in una directory \ml{hol}\footnote{Si pu�
46 {\tt sigobj} & Directory per i file object \ML{} & Directory\\
96 Se questi file sono in \texttt{/usr/lib}, non c'� bisogno di cambiare nulla, ma altre posizioni possono richiedere un'ulteriore configurazione di sistema.
97 Un esempio di comando di inizializzazione di \texttt{LD\_LIBRARY\_PATH} (in un file come \texttt{.bashrc}) potrebbe essere
110 - [opening file "tools/smart-configure-mosml.sml"]
162 creare un file richiamato per fornire i valori corretti. Con Moscow~ML, questo
165 nella directory \texttt{tools-poly}. In questo file, si specifichi il
179 Il file \texttt{config-override} ha bisogno di fornire soli i valori per quelle
182 Con questo file nel posto corretto, il programma \texttt{smart-configure} user�
191 In circostanze estreme � possibile modificare il file
[all...]
H A Dmore-examples.tex37 con il suo sistema di tipi. I file furono sviluppati originariamente da Tom Melham
47 Questo file illustra l'implementazione di John Harrison di
62 Questa sotto directory contiene i file usati nell'esempio di parit� del
/seL4-l4v-master/HOL4/help/src-sml/
H A DMyDatabase.sml16 type entry = { comp : component, file : string, line : int }
81 fun getname ({comp, file, ...} : entry) =
83 Str => file
H A DDatabase.sig13 type entry = { comp : component, file : string, line : int }
H A DMyDatabase-sig.sml16 type entry = { comp : component, file : string, line : int }
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/Examples/
H A DmlEdit.sml173 file = "",
184 | SOME {file, ...} =>
189 val f = TextIO.openIn file
195 (* Should we save any existing file? *)
200 fileName=file})
203 SOME(concat["Unable to open - ", file, "\n"(*, exnMessage exn*)]),
210 then (* Save to the original file name if there is one. *)
222 (LRESINT 0, (* Use the selected file name. *)
503 (* Write the document to the given file name. *)
505 (* Write the file a
[all...]
/seL4-l4v-master/HOL4/examples/dev/sw/
H A Dgr.sml4 * COPYRIGHT (c) 1997 by Martin Erwig. See COPYRIGHT file for details.
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A Dgr.sml4 * COPYRIGHT (c) 1997 by Martin Erwig. See COPYRIGHT file for details.
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/util/
H A Dgr.sml4 * COPYRIGHT (c) 1997 by Martin Erwig. See COPYRIGHT file for details.
/seL4-l4v-master/HOL4/src/opentheory/postbool/
H A DOpenTheoryIO.sml44 val t = Curl.submitFile {url=url,field="article",file=t}
/seL4-l4v-master/HOL4/src/portableML/
H A DPIntMap.sig14 * (enclosed in the file LGPL).
/seL4-l4v-master/isabelle/src/Pure/Tools/
H A Dmkroot.scala36 if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
39 if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
/seL4-l4v-master/HOL4/polyml/Tests/
H A DRunTests.sml13 (* Run a file. Returns true if it succeeds, false if it fails. *)
111 val testPath = joinDirFile{dir=parentDir, file=dirName}
146 if runTest(joinDirFile{dir=testPath, file=f})
148 else (print "Failed!!\n"; runDir(files, fails @ [joinDirFile{dir=dirName, file=f}]))
/seL4-l4v-master/HOL4/examples/
H A DtempScript.sml5 * for theory "x", you must change the name of this file to "xScript.sml", *
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/
H A Dmkroot.scala36 if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
39 if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
/seL4-l4v-master/HOL4/src/1/
H A DDiskThms.sml31 | _ => raise Fail "Couldn't parse sexp from file"
/seL4-l4v-master/HOL4/src/TeX/
H A Dholindex.sml14 (* Parse the input file *)
19 val file = "/home/tt291/Documents/thesis/holmunge/test.hix";
103 | ["Overrides", file] =>
104 (mungeTools.user_overrides := mungeTools.read_overrides file;
122 val file = if Path.isAbsolute filename then filename else value
124 val entryL = AssembleHolindexParser.parse_hdf_file file;
155 fun parse_hix file =
158 val fh = Portable.open_in file;
159 val basedir = Path.dir file;
540 val file
[all...]
H A Dholindex-demo.tex19 \setHOLoverrides{file} %optional
91 Definitions like these inside a latex file are tedious,
93 an external file for all these definitions. There
103 label = "a short description of term form external file",
110 label = "a short description of the type from external file",
146 %use external file
246 line to the header of your file:
255 definitions are printed. Just copy them to the header of your file
/seL4-l4v-master/HOL4/examples/HolBdd/
H A DVarmap.sml11 (* Thu Oct 4 15:45:52 BST 2001 -- created file *)
13 (* Thu Mar 28 09:40:05 GMT 2002 -- added signature file *)
/seL4-l4v-master/HOL4/polyml/mlsource/extra/Win/
H A DDragDrop.sml41 (* Call DragQueryFile to get the file(s). *)
65 (* Call DragQueryPoint to find out where to drop the file(s). *)
/seL4-l4v-master/isabelle/src/Pure/Admin/
H A Dcomponents.scala90 File.find_files(dir.file,
91 (file: JFile) => file.isDirectory && purge_set(file.getName),
/seL4-l4v-master/isabelle/src/Pure/System/
H A Disabelle_fonts.scala40 lazy val font: Font = Font.createFont(Font.TRUETYPE_FONT, path.file)
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A Dselftest.sml27 fun test_file file = let
29 val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) []));

Completed in 167 milliseconds

1234567891011>>