]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/dependenciesParser.mli
Huge commit with several changes:
[helm.git] / helm / software / components / grafite_parser / dependenciesParser.mli
index 6a8d2ae212bbfb17495fc0af3be6ce82cfe2c275..57529966b9bd5e84c6658e51c52081a1490b4594 100644 (file)
@@ -28,13 +28,9 @@ exception UnableToInclude of string
   (* statements meaningful for matitadep *)
 type dependency =
   | IncludeDep of string
-  | BaseuriDep of string
   | UriDep of UriManager.uri
+  | InlineDep of string
 
 val pp_dependency: dependency -> string
 
-  (** @raise End_of_file *)
-val parse_dependencies: Ulexing.lexbuf -> dependency list
-
-(* returns baseuri and the full path of the script *)
-val baseuri_of_script : include_paths:string list -> string -> string * string
+val deps_of_file: string -> dependency list